Syntax for free: representing syntax with binding using parametricity

Atkey, Robert; Curien, Pierre-Louis, ed. (2009) Syntax for free: representing syntax with binding using parametricity. In: Typed Lambda Calculi and Applications, 9th International Conference, TLCA 2009. Lecture Notes in Computer Science, 5608 . Springer, pp. 35-49. ISBN 978-3-642-02272-2 (https://doi.org/10.1007/978-3-642-02273-9_5)

Preview

PDF. Filename: syntaxforfree.pdf Accepted Author Manuscript Download (198kB)| Preview

Abstract

We show that, in a parametric model of polymorphism, the type ∀ α. ((α → α) → α) → (α → α → α) → α is isomorphic to closed de Bruijn terms. That is, the type of closed higher-order abstract syntax terms is isomorphic to a concrete representation. To demonstrate the proof we have constructed a model of parametric polymorphism inside the Coq proof assistant. The proof of the theorem requires parametricity over Kripke relations. We also investigate some variants of this representation.

ORCID iDs

Atkey, Robert ORCID: https://orcid.org/0000-0002-4414-5047

• 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:	34483
  Dates:	Date Event 2009 Published
  Subjects:	Science > Mathematics > Electronic computers. Computer science
  Department:	Faculty of Science > Computer and Information Sciences
  Depositing user:	Pure Administrator
  Date deposited:	12 Nov 2011 11:05
  Last modified:	28 Nov 2024 01:29
  Related URLs:	Journal or Publication Author
  URI:	https://strathprints.strath.ac.uk/id/eprint/34483