Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. In this talk, I will survey the proof environment Beluga. To specify formal systems and represent derivations within them, Beluga relies on the logical framework LF; to reason about formal systems, Beluga provides a dependently typed functional language for implementing (co)inductive proofs about derivation trees as (co)recursive functions following the Curry-Howard isomorphism. Key to this approach is the ability to model derivation trees that depend on a context of assumptions using a generalization of the logical framework LF, i.e. contextual LF which supports first-class contexts and simultaneous substitutions. Using several examples, I show how Beluga enables direct and compact mechanizations of the meta-theory of formal systems, in particular programming languages and logics.

Bio: Brigitte Pientka is an Associate Professor in the School of Computer Science at McGill University, Montreal, Canada. She received her Ph.D. from Carnegie Mellon University (Pittsburgh, USA) in 2003. Currently, she is a Humboldt Research Fellow at the Ludwig-Maximilian University Munich, Germany. Her research interest lies in developing a theoretical and practical foundation for building and reasoning about reliable safe software systems. To achieve this goal, she combines theoretical research on the logical foundations of computer science in programming languages and verification with system building.