License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2016.1
URN: urn:nbn:de:0030-drops-98603
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9860/
Go to the corresponding LIPIcs Volume Portal

Miller, Dale

Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper)

pdf-format:
LIPIcs-TYPES-2016-1.pdf (0.4 MB)

Abstract

Proof assistants and the programming languages that implement them need to deal with a range of linguistic expressions that involve bindings. Since most mature proof assistants do not have built-in methods to treat this aspect of syntax, many of them have been extended with various packages and libraries that allow them to encode bindings using, for example, de Bruijn numerals and nominal logic features. I put forward the argument that bindings are such an intimate aspect of the structure of expressions that they should be accounted for directly in the underlying programming language support for proof assistants and not added later using packages and libraries. One possible approach to designing programming languages and proof assistants that directly supports such an approach to bindings in syntax is presented. The roots of such an approach can be found in the mobility of binders between term-level bindings, formula-level bindings (quantifiers), and proof-level bindings (eigenvariables). In particular, by combining Church's approach to terms and formulas (found in his Simple Theory of Types) and Gentzen's approach to sequent calculus proofs, we can learn how bindings can declaratively interact with the full range of logical connectives and quantifiers. I will also illustrate how that framework provides an intimate and semantically clean treatment of computation and reasoning with syntax containing bindings. Some implemented systems, which support this intimate and built-in treatment of bindings, will be briefly described.

BibTeX - Entry

@InProceedings{miller:LIPIcs:2018:9860,
  author =	{Dale Miller},
  title =	{{Mechanized Metatheory Revisited: An Extended Abstract (Invited Paper)}},
  booktitle =	{22nd International Conference on Types for Proofs and  Programs (TYPES 2016)},
  pages =	{1:1--1:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Silvia Ghilezan and Herman Geuvers and Jelena Ivetić},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9860},
  URN =		{urn:nbn:de:0030-drops-98603},
  doi =		{10.4230/LIPIcs.TYPES.2016.1},
  annote =	{Keywords: mechanized metatheory, mobility of binders, lambda-tree syntax, higher-order abstract syntax}
}

Keywords: mechanized metatheory, mobility of binders, lambda-tree syntax, higher-order abstract syntax
Collection: 22nd International Conference on Types for Proofs and Programs (TYPES 2016)
Issue Date: 2018
Date of publication: 05.11.2018

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