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
|
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 |
Official URL: https://doi.org/10.1145/3018610.3018613
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 ![]() ![]() ![]() | 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: | 20 Jan 2021 15:57 |
Related URLs: | |
URI: | https://strathprints.strath.ac.uk/id/eprint/59447 |
Export data: |
CORE (COnnecting REpositories)