Type-and-scope safe programs and their proofs

Guillaume Allais, James Chapman, Conor McBride, James McKinna

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Citations (Scopus)

Abstract

We abstract the common type-and-scope safe structure from computations on terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing with a name supply. By exposing this structure, we can prove generic simulation and fusion lemmas relating operations built this way. This work has been fully formalised in Agda.

Original languageEnglish
Title of host publicationCPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
EditorsYves Bertot, Viktor Vafeiadis
PublisherAssociation for Computing Machinery
Pages195-207
Number of pages13
ISBN (Electronic)9781450347051
DOIs
Publication statusPublished - 16 Jan 2017
Event6th ACM SIGPLAN Conference on Certified Programs and Proofs 2017 - Paris, France
Duration: 16 Jan 201717 Jan 2017

Conference

Conference6th ACM SIGPLAN Conference on Certified Programs and Proofs 2017
Abbreviated titleCPP 2017
CountryFrance
CityParis
Period16/01/1717/01/17

Keywords

  • Agda
  • Generic programming
  • Lambda-calculus
  • Mechanized meta-theory
  • Normalisation by evaluation
  • Semantics

ASJC Scopus subject areas

  • Software
  • Computer Science Applications

Fingerprint Dive into the research topics of 'Type-and-scope safe programs and their proofs'. Together they form a unique fingerprint.

  • Cite this

    Allais, G., Chapman, J., McBride, C., & McKinna, J. (2017). Type-and-scope safe programs and their proofs. In Y. Bertot, & V. Vafeiadis (Eds.), CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (pp. 195-207). Association for Computing Machinery. https://doi.org/10.1145/3018610.3018613