2026-08-16T12:00:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5177 2024-03-06T10:29:46Z ddc:004 open_access

Mechanizing Meta-Theory in Beluga (Invited Talk) Pientka, Brigitte Type systems Dependent Types Logical Frameworks 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Brigitte Pientka 2015 Is Part Of OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.WPTE.2015.1 urn:nbn:de:0030-drops-51770 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.1 eng https://creativecommons.org/licenses/by/3.0/legalcode