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

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

Download (158kB)| Preview

    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.

    ORCID iDs

    Allais, Guillaume ORCID logoORCID: https://orcid.org/0000-0002-4091-657X, Chapman, James ORCID logoORCID: https://orcid.org/0000-0001-9036-8252, McBride, Conor ORCID logoORCID: https://orcid.org/0000-0003-1487-0886 and McKinna, James; Bertot, Yves and Vafeiadis, Viktor