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, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
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.
Type de document :
Communication dans un congrès
Post-proceedings of TYPES 2016 , 2017, Novi Sad, Serbia. 〈10.4230/LIPIcs〉
Liste complète des métadonnées

Littérature citée [78 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01615681
Contributeur : Dale Miller <>
Soumis le : jeudi 12 octobre 2017 - 16:31:22
Dernière modification le : jeudi 10 mai 2018 - 02:06:39

Fichier

mmr-types.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

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

Partager

Métriques

Consultations de la notice

194

Téléchargements de fichiers

68