A formalized general theory of syntax with bindings

Conference paper

Gheri, L. and Popescu, A. 2017. A formalized general theory of syntax with bindings. 8th International Conference Interactive Theorem Proving. Brasilia, Brazil 26 - 29 Sep 2017 Cham Springer International Publishing. pp. 241-261 https://doi.org/10.1007/978-3-319-66107-0_16
TypeConference paper
TitleA formalized general theory of syntax with bindings
AuthorsGheri, L. and Popescu, A.
Abstract

We present the formalization of a theory of syntax with bindings that has been developed and refined over the last decade to support several large formalization efforts. Terms are defined for an arbitrary number of constructors of varying numbers of inputs, quotiented to alpha-equivalence and sorted according to a binding signature. The theory includes a rich collection of properties of the standard operators on terms, such as substitution and freshness. It also includes induction and recursion principles and support for semantic interpretation, all tailored for smooth interaction with the bindings and the standard operators.

Conference8th International Conference Interactive Theorem Proving
Page range241-261
ISSN0302-9743
ISBN
Hardcover9783319661063
PublisherSpringer International Publishing
Place of publicationCham
Publication dates
Print01 Jun 2017
Online21 Aug 2017
Publication process dates
Deposited22 Jan 2018
Accepted01 Mar 2017
Output statusPublished
Accepted author manuscript
Copyright Statement

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-66107-0_16

Additional information

Paper published as:
Gheri L., Popescu A. (2017) A Formalized General Theory of Syntax with Bindings. In: Ayala-Rincón M., Muñoz C. (eds) Interactive Theorem Proving. ITP 2017. Lecture Notes in Computer Science, vol 10499. Springer, Cham

Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-319-66107-0_16
LanguageEnglish
Book titleInteractive Theorem Proving: 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings. Lecture Notes in Computer Science, vol 10499
Permalink -

https://repository.mdx.ac.uk/item/87690

Log in to edit

Download files

Accepted author manuscript
ITP2017.pdf

  • 9
    total views
  • 0
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as