Picture map of Europe with pins indicating European capital cities

Open Access research with a European policy impact...

The Strathprints institutional repository is a digital archive of University of Strathclyde's Open Access research outputs. Strathprints provides access to thousands of Open Access research papers by Strathclyde researchers, including by researchers from the European Policies Research Centre (EPRC).

EPRC is a leading institute in Europe for comparative research on public policy, with a particular focus on regional development policies. Spanning 30 European countries, EPRC research programmes have a strong emphasis on applied research and knowledge exchange, including the provision of policy advice to EU institutions and national and sub-national government authorities throughout Europe.

Explore research outputs by the European Policies Research Centre...

Strathprints

Type-and-scope safe programs and their proofs

Allais, Guillaume and Chapman, James and McBride, Conor and McKinna, James (2017) Type-and-scope safe programs and their proofs. In: CPP 2017. ACM, New York, NY, New York. 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.

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: 21 Sep 2017 15:03
Related URLs:
URI: https://strathprints.strath.ac.uk/id/eprint/59447
Export data:
CORE (COnnecting REpositories)