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 book

18 Citations (Scopus)
85 Downloads (Pure)


We abstract the common type-and-scope safe structure fromcomputations on lambda-terms that deliver, e.g., renaming, substitution, evaluation, CPS-transformation, and printing witha 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
Subtitle of host publicationProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
EditorsYves Bertot, Viktor Vafeiadis
Place of PublicationNew York
Number of pages13
Publication statusPublished - 16 Jan 2017
Event6th ACM SIGPLAN Conference on Certified Programs and Proofs - Paris, France
Duration: 16 Jan 201717 Jan 2017
Conference number: 6th


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


  • agda
  • dependently typed functional type
  • formal verification
  • lambda calculus
  • normalization by evaluation
  • syntax
  • semantics
  • mechanized meta theory
  • generic programming


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

Cite this