Functional programming and dependent types, automated theorem proving (ATP), logic (modal) systems and technologies for the semantic web.
Functional programming, dependent types:
I'm interested in development of programming paradigms that allow to write programs in such a way so that their correctness could be formally proven. The most often used procedural programs
are almost impossible to automatically verify efficiently. Alas, current trends in commercial programming even promote techniques that result in messy programs for which little verification is done at compile time. On the other hand functional programs can be analyzed much easier, have strong typing systems and promote much healthier programming techniques. Still todays functional languages lack direct connection to methods of formal automated verification.
Dependently typed functional languages provide a way how to write such correct programs. Typing systems in such languages are powerful enough to state quantified propositions about expressions. Types correspond to propositions about expressions type-checking guarantees that expressions comply to the types.
Automated theorem proving:
Development of automated theorem proving tools and techniques how to efficiently use ATP provers. Especially for reasoning within large theories, where many conjectures are to be proved from the same (or similar) sets of axioms. These techniques include analyzing the structure of theories, lemma generation and selection, determining the optimal set of premises for proving conjectures, etc.
Using ATP tools for deciding formulae in various propositional logic systems (with emphasis on modal systems) and for deciding relationships between between logic systems. This is particularly challenging task for ATP systems, with variety of problems with different level of complexity.
: Technologies that offer advanced possibilities of using WWW
for communicating, collaborating and sharing knowledge over the Internet.