Mechanized Metatheory Revisited: An Extended Abstract

Dale Miller 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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 (quanti-fiers), 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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [78 references]  Display  Hide  Download

https://hal.inria.fr/hal-01615681
Contributor : Dale Miller <>
Submitted on : Thursday, October 12, 2017 - 4:31:22 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM

File

mmr-types.pdf
Files produced by the author(s)

Identifiers

Citation

Dale Miller. Mechanized Metatheory Revisited: An Extended Abstract . Post-proceedings of TYPES 2016 , 2017, Novi Sad, Serbia. 〈10.4230/LIPIcs〉. 〈hal-01615681〉

Share

Metrics

Record views

228

Files downloads

95