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 language | English |
|---|---|
| Title of host publication | CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs |
| Editors | Yves Bertot, Viktor Vafeiadis |
| Publisher | Association for Computing Machinery |
| Pages | 195-207 |
| Number of pages | 13 |
| ISBN (Electronic) | 9781450347051 |
| DOIs | |
| Publication status | Published - 16 Jan 2017 |
| Event | 6th ACM SIGPLAN Conference on Certified Programs and Proofs 2017 - Paris, France Duration: 16 Jan 2017 → 17 Jan 2017 |
Conference
| Conference | 6th ACM SIGPLAN Conference on Certified Programs and Proofs 2017 |
|---|---|
| Abbreviated title | CPP 2017 |
| Country/Territory | France |
| City | Paris |
| Period | 16/01/17 → 17/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
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver