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

31 Citations (Scopus)


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
Number of pages13
ISBN (Electronic)9781450347051
Publication statusPublished - 16 Jan 2017
Event6th ACM SIGPLAN Conference on Certified Programs and Proofs 2017 - Paris, France
Duration: 16 Jan 201717 Jan 2017


Conference6th ACM SIGPLAN Conference on Certified Programs and Proofs 2017
Abbreviated titleCPP 2017


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

ASJC Scopus subject areas

  • Software
  • Computer Science Applications


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

Cite this