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.

• 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
• Item metadata

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