Research Interests

My research interest lies in developing a theoretical and practical foundation for building and reasoning about reliable safe software systems. To achieve this goal, I combine theoretical research on the logical foundations of computer science in programming languages and verification with system building. The topics I am interested in include logics (classical and non-classical), type theory, theorem proving, logic and functional programming, and logical frameworks.

For more information, you can visit Computation and Logic group.

Recent Publications

For a list of all publications see Research.

Recent Drafts

Software release

  • Beluga - Version 0.6 (13 February 2014) dependently-typed programming and proof environment built on top of the logical framework LF. This verion includes computation-level data types, type reconstruction, supports context subsumption, provides an interpreter and coverage checker.

Professional Activities

Talks

Program Chair

  • International Conference on Typed Lambda Calculi and Applications (TLCA'16), 2016, Portugal.

Conference Chair

  • 22nd International Conference on Automated Deduction (CADE'09)

Editor

  • Editorial Board of Journal of Functional Programming
  • Guest Editor for a special issue in Journal of Automated Reasoning for the best papers of CADE-22 (Co-editor with Renate Schmidt)
  • Guest Editor for a special issue in Information and Computation on Intuitionistic Modal Logics and Applications (IMLA) (Co-editor with Valeria de Paiva)

Program Committee

  • 41st ACM Symposium on Principles of Programming Languages (POPL 2015)
  • Joint 25th International Conference on Rewriting Techniques and Applications and 12th International Conference on Typed Lambda Calculi and Applications (RTA-TLCA'14), Vienna, Austria, July 2014
  • International Workshop on Logical Frameworks and Meta-Languages: theory and practice (LFMTP'14), July 2014, Vienna, Austria, as part of FLOC co-located with LICS'14 and IJCAR'14
  • International Workshop on Logical Frameworks and Meta-Languages: theory and practice (LFMTP'13), Sept 2013, Boston, USA, co-located with ICFP'13.
  • ACM Sigplan Workshop on Dependently typed programming (DTP'13), Sept 2013, Boston, USA, co-located with ICFP'13.
  • 2nd ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE'13), Sept 2013, Boston, USA, co-located with ICFP'13.
  • 24th International Joint Conference on Automated Deduction (CADE-24), Lake Placid, USA, June 2013
  • International Conference on Interactive Theorem Proving (ITP'13), Rennes, France, Aug 2013
  • International Conference on Interactive Theorem Proving (ITP'12), Princeton, USA, Aug 2012
  • 17th ACM SIGPLAN International Conference on Functional Programming (ICFP'12)
  • CiE 2012: Turing Centenary Conference: How the world computes, Cambrigde, England (PC)
  • 39th ACM Symposium on Principles of Programming Languages (POPL 2012), Extended Review Committee
  • First International Conference on Certified Programs and Proofs (CPP 2011), co-located with APLAS'11, Taiwan, Dec 2011
  • International Conference on Interactive Theorem Proving (ITP'11), Nijmegen, Netherlands, Aug 2011
  • 23rd International Joint Conference on Automated Deduction (CADE-23), 2011, Waslaw, Poland, July 2011
  • 5th International Joint Conference on Automated Reasoning (IJCAR-10)
  • International Conference on Interactive Theorem Proving (ITP-10)
  • 26th International Conference on Mathematical Foundations of Programming Semantics (MFPS) (MFPS-10)
  • 19th International Workshop on Functional and (Constraint) Logic Programming (WFLP'10)
  • 22nd International Conference on Automated Deduction (CADE'09)
  • International Workshop on Proof-Search in Type Theories (PSTT'09)
  • 7th International Workshop on the Implementation of Logics (IWIL'08)
  • 13th ACM SIGPLAN International Conference on Functional Programming (ICFP'08)
  • 24th International Conference on Logic Programming (ICLP'08)
  • International Workshop on Logical Frameworks and Meta-Languages: theory and practice (LFMTP'08)

Professional Organizations


Design downloaded from Free Templates
Picture taken by B.Pientka and D.Schlimm: Montreal, Biosphere