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

33 Citations (Scopus)
139 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
Country/TerritoryFrance
CityParis
Period16/01/1717/01/17
Internet address

Keywords

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

Fingerprint

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

Cite this