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.

News and Upcoming Events

  • Support our Seeds of Change Campaign to send McGill students to the Grace Hopper Celebration!
  • I have been awarded a Humboldt Fellowship! Starting September I will be spending the next year at the Ludwig-Maximilian University Munich, Germany.
  • I am the co-PC chair for Formal Structures for Computation and Deduction (FSCD'16), 2016! Submit your paper!
  • I am one of the invited speakers for 32nd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXII) in Pittsburgh in May 2016.
  • I am on the Program Committee of the Workshop on Type Directed Programming, co-located with ICFP'16.

Recent Publications

For a list of all publications see Research.

Recent Drafts

Software release

  • Beluga - Version 0.8.3 (09 March 2015) dependently-typed programming and proof environment built on top of the logical framework LF. This version includes computation-level data types, type reconstruction, supports context subsumption, provides an interpreter and coverage checker.

Professional Activities

Talks

Program Chair

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)

Recent Program Committee

  • 42nd ACM Symposium on Principles of Programming Languages (POPL 2016), Extended Review Committee
  • 25rd International Conference on Automated Deduction (CADE-25), Berlin, Germany, 2015
  • 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

Professional Organizations


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