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

13 Citations (Scopus)
80 Downloads (Pure)

Abstract

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
DOIs
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
http://cpp2017.mpi-sws.org/index.html

Conference

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

    Fingerprint

Keywords

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

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 New York. https://doi.org/10.1145/3018610.3018613