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

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.

ORCID iDs

Allais, Guillaume

, Chapman, James

, McBride, Conor

and McKinna, James; Bertot, Yves and Vafeiadis, Viktor

Citations and altmetrics

Item metadata

Item type:	Book Section
ID code:	59447
Dates:	Date Event 16 January 2017 Published 10 December 2016 Accepted 14 October 2016 Submitted
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:	03 Mar 2021 03:52
Related URLs:	Event Journal or Publication
URI:	https://strathprints.strath.ac.uk/id/eprint/59447

Export

CORE (COnnecting REpositories)