The Programming Languages Research Group conducts research in the area of the theoretical foundations and formal semantics of programming languages, program analysis and verification, and automated theorem proving. In our work we use the methods of mathematical logic and universal algebra as well as tools such as functional language implementations and proof assistants. The research projects carried out by the team concern the following topics:

  • methods of reasoning about programs in decidable fragments of logic
  • deductive verification for concurrency
  • categorical semantics of programming languages with computational effects
  • operational semantics of higher-order programming languages
  • methods of reasoning about program equivalence in higher-order languages
  • program transformation
  • the Curry-Howard isomorphism for classical and modal logics
  • type-and-effect systems
  • automated theorem proving in classical logic with partial functions
  • geometric resolution