Type-and-scope safe programs and their proofs

Allais, Guillaume and Chapman, James and McBride, Conor and McKinna, James; Bertot, Yves and Vafeiadis, Viktor, eds. (2017) Type-and-scope safe programs and their proofs. In: CPP 2017. ACM, New York, NY, FRA. ISBN 9781450347051 (https://doi.org/10.1145/3018610.3018613)

[thumbnail of Allais-etal-CPP-2017-Type-and-scope-safe-programs]
Text. Filename: Allais_etal_CPP_2017_Type_and_scope_safe_programs.pdf
Accepted Author Manuscript

Download (158kB)| Preview


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.