Home > News > Brigitte Pientka: Mechanizing Meta-Theory in Beluga

Brigitte Pientka: Mechanizing Meta-Theory in Beluga

Date: 25. 5. 2020
Source: Mathematics and theoretical computing seminar
ńĆetrtek, 28. 5. 2020, od 16:00 do 17:00 , spletni seminar

Zoom ID 989 0478 8985

Brigitte Pientka (McGill University) 

After the talk, the video recording will be made available. 

Abstract: 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.

Our experience demonstrated that Beluga enables direct and compact mechanizations of the meta-theory of formal systems, in particular programming languages and logics.