License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.WPTE.2015.1
URN: urn:nbn:de:0030-drops-51770
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5177/
Go to the corresponding OASIcs Volume Portal

Pientka, Brigitte

Mechanizing Meta-Theory in Beluga (Invited Talk)

pdf-format:
3.pdf (0.3 MB)

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.

BibTeX - Entry

@InProceedings{pientka:OASIcs:2015:5177,
  author =	{Brigitte Pientka},
  title =	{{Mechanizing Meta-Theory in Beluga (Invited Talk)}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{1--1},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Yuki Chiba and Santiago Escobar and Naoki Nishida and David Sabel and Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5177},
  URN =		{urn:nbn:de:0030-drops-51770},
  doi =		{10.4230/OASIcs.WPTE.2015.1},
  annote =	{Keywords: Type systems, Dependent Types, Logical Frameworks}
}

Keywords: Type systems, Dependent Types, Logical Frameworks
Collection: 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)
Issue Date: 2015
Date of publication: 17.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI