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.

ORCID iDs

Allais, Guillaume ORCID: https://orcid.org/0000-0002-4091-657X

Chapman, James ORCID: https://orcid.org/0000-0001-9036-8252

McBride, Conor ORCID: https://orcid.org/0000-0003-1487-0886

• Share and Export
  

  RDF+XMLBibTeXRIOXX2 XMLRDF+N-TriplesJSONDublin CoreAtomSimple MetadataReferMETSHTML CitationASCII CitationOpenURL ContextObjectEndNoteOpenURL ContextObject in SpanMODSMPEG-21 DIDLEP3 XMLData Cite XMLRIS (EndNote Online, Zotero, Ref manager, etc)RDF+N3Multiline CSV
• 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:	28 Nov 2021 02:22
  Related URLs:	Event Journal or Publication
  URI:	https://strathprints.strath.ac.uk/id/eprint/59447