Mechanizing Meta-Theory in Beluga (Invited Talk) ...
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 pr...
| Main Author: | |
|---|---|
| Format: | Conference Object |
| Language: | English |
| Published: |
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2015
|
| Subjects: | |
| Online Access: | https://dx.doi.org/10.4230/oasics.wpte.2015.1 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.1 |
| Summary: | 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 ... : OASIcs, Vol. 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015), pages 1-1 ... |
|---|