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+XMLRDF+N3EP3 XMLMETSASCII CitationRefWorksMultiline CSVRDF+N-TriplesReferDublin CoreRIOXX2 XMLSimple MetadataOpenURL ContextObject in SpanHTML CitationEndNoteMODSRIS (EndNote Online, Zotero, Ref manager, etc)JSONAtomMPEG-21 DIDLData Cite XMLBibTeXOpenURL ContextObject
• 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:	15 Dec 2024 01:06
  Related URLs:	Event Journal or Publication
  URI:	https://strathprints.strath.ac.uk/id/eprint/59447