Mechanizing Meta-Theory in Beluga (Invited Talk)

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 provides a sophisticated infrastructure based on the logical framework LF; in particular, its infrastructure not only supports modelling binders via binders in LF, but extends and generalizes LF with first-class contexts to abstract over a set of assumptions, contextual objects to model derivations that depend on assumptions, and first-class simultaneous substitutions to relate contexts. These extensions allow us to directly support key and common concepts that frequently arise when describing formal systems and derivations within them. 

To reason about formal systems, Beluga provides a dependently typed functional language for implementing inductive proofs about derivations as recursive functions on contextual objects following the Curry-Howard isomorphism.  Recently, the Beluga system has also been extended with a totality checker which guarantees that recursive programs are well-founded and correspond to inductive proofs and an interactive program development environment to support incremental proof / program construction. Taken together these extensions enable direct and compact mechanizations. To demonstrate Beluga's strength, we develop a weak normalization proof using logical relations. The Beluga system together with examples is available from http://complogic.cs.mcgill.ca/beluga.