Brigitte Pientka – Mechanizing Meta Theory in Beluga
Channel: FMF Foundations seminar
Date: 2021-11-02

Mechanizing Meta-Theory in Beluga

Time: Thursday, May 28, 2020
Speaker: Brigitte Pientka (McGill University)
Proof assistant: http://complogic.cs.mcgill.ca/beluga/

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.