Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders

Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders

We introduce a universe of regular datatypes with variable binding information, for which we define generic formation and elimination (i.e. induction /recursion) operators. We then define a generic alpha-equivalence relation over the types of the universe based on name-swapping, and derive iteratio...

Full description

Bibliographic Details
Main Authors: Ernesto Copello, Nora Szasz, Álvaro Tasistro
Format: Article
Language:English
Published: Open Publishing Association 2018-07-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1807.01870v1
id doaj-fa5114a1eeab49e8a7ee3d22bb0b8bb3
record_format Article
spelling doaj-fa5114a1eeab49e8a7ee3d22bb0b8bb32020-11-25T01:49:22ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802018-07-01274Proc. LFMTP 2018112610.4204/EPTCS.274.2:5Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with BindersErnesto Copello0Nora Szasz1Álvaro Tasistro2 University of Iowa Universidad ORT Uruguay Universidad ORT Uruguay We introduce a universe of regular datatypes with variable binding information, for which we define generic formation and elimination (i.e. induction /recursion) operators. We then define a generic alpha-equivalence relation over the types of the universe based on name-swapping, and derive iteration and induction principles which work modulo alpha-conversion capturing Barendregt's Variable Convention. We instantiate the resulting framework so as to obtain the Lambda Calculus and System F, for which we derive substitution operations and substitution lemmas for alpha-conversion and substitution composition. The whole work is carried out in Constructive Type Theory and machine-checked by the system Agda.http://arxiv.org/pdf/1807.01870v1
collection DOAJ
language English
format Article
sources DOAJ
author Ernesto Copello
Nora Szasz
Álvaro Tasistro
spellingShingle Ernesto Copello
Nora Szasz
Álvaro Tasistro
Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders
Electronic Proceedings in Theoretical Computer Science
author_facet Ernesto Copello
Nora Szasz
Álvaro Tasistro
author_sort Ernesto Copello
title Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders
title_short Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders
title_full Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders
title_fullStr Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders
title_full_unstemmed Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders
title_sort formalisation in constructive type theory of barendregt's variable convention for generic structures with binders
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2018-07-01
description We introduce a universe of regular datatypes with variable binding information, for which we define generic formation and elimination (i.e. induction /recursion) operators. We then define a generic alpha-equivalence relation over the types of the universe based on name-swapping, and derive iteration and induction principles which work modulo alpha-conversion capturing Barendregt's Variable Convention. We instantiate the resulting framework so as to obtain the Lambda Calculus and System F, for which we derive substitution operations and substitution lemmas for alpha-conversion and substitution composition. The whole work is carried out in Constructive Type Theory and machine-checked by the system Agda.
url http://arxiv.org/pdf/1807.01870v1
work_keys_str_mv AT ernestocopello formalisationinconstructivetypetheoryofbarendregtsvariableconventionforgenericstructureswithbinders
AT noraszasz formalisationinconstructivetypetheoryofbarendregtsvariableconventionforgenericstructureswithbinders
AT alvarotasistro formalisationinconstructivetypetheoryofbarendregtsvariableconventionforgenericstructureswithbinders
_version_ 1725006947376168960

Similar Items