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

[img]
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.

    Creators(s): 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
    Item type:Book Section
    ID code:59447
    Keywords:agda, dependently typed functional type , formal verification, lambda calculus, normalization by evaluation , syntax, semantics, mechanized meta theory, generic programming, Library Science. Information Science, Electronic computers. Computer science, Computer Science (miscellaneous), Computational Theory and Mathematics, Software
    Subjects:Bibliography. Library Science. Information Resources > Library Science. Information Science
    Science > Mathematics > Electronic computers. Computer science
    Department:Faculty of Science > Computer and Information Sciences
    Depositing user: Pure Administrator
    Date deposited:17 Jan 2017 09:23
    Last modified:19 Feb 2020 08:44
    Related URLs:
    URI:https://strathprints.strath.ac.uk/id/eprint/59447
    Export data:
    CORE (COnnecting REpositories)