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 (ITP). Brasília, Brazil 26 - 29 Sep 2017 Springer. 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.

Research GroupFoundations of Computing group
Conference8th International Conference Interactive Theorem Proving (ITP)
Page range241-261
ISSN0302-9743
ISBN
Hardcover9783319661063
PublisherSpringer
Publication dates
Online21 Aug 2017
Print29 Sep 2017
Publication process dates
Deposited20 Jun 2017
Accepted04 Jun 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

Cite this paper 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
Permalink -

https://repository.mdx.ac.uk/item/870wq

Log in to edit

Download files

Accepted author manuscript
bindings.pdf

  • 20
    total views
  • 10
    total downloads
  • 1
    views this month
  • 0
    downloads this month

Export as