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)
Preview |
Text.
Filename: 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.
-
-
Item type: Book Section ID code: 59447 Dates: DateEvent16 January 2017Published10 December 2016Accepted14 October 2016SubmittedSubjects: Bibliography. Library Science. Information Resources > Library Science. Information Science
Science > Mathematics > Electronic computers. Computer scienceDepartment: Faculty of Science > Computer and Information Sciences Depositing user: Pure Administrator Date deposited: 17 Jan 2017 09:23 Last modified: 16 Apr 2024 00:04 Related URLs: URI: https://strathprints.strath.ac.uk/id/eprint/59447
CORE (COnnecting REpositories)