Syntax for Free: Representing Syntax with Binding Using Parametricity

Reference. Syntax for Free: Representing Syntax with Binding Using Parametricity

Cite

Cite as @atkey-2009-syntax (helia, typst) · \cite{atkey-2009-syntax} (LaTeX)

BibTeX

bibtex · 1 line

@inbook{atkey-2009-syntax, title={Syntax for Free: Representing Syntax with Binding Using Parametricity}, ISBN={9783642022739}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-642-02273-9_5}, DOI={10.1007/978-3-642-02273-9_5}, booktitle={Typed Lambda Calculi and Applications}, publisher={Springer Berlin Heidelberg}, author={Atkey, Robert}, year={2009}, pages={35–49} }

hayagriva YAML (typst)

yaml · 15 lines

atkey-2009-syntax:
  type: chapter
  title: 'Syntax for Free: Representing Syntax with Binding Using Parametricity'
  author: Atkey, Robert
  date: 2009
  page-range: 35-49
  url: http://dx.doi.org/10.1007/978-3-642-02273-9_5
  serial-number:
    doi: 10.1007/978-3-642-02273-9_5
    isbn: '9783642022739'
    issn: 1611-3349
  parent:
    type: book
    title: Typed Lambda Calculi and Applications
    publisher: Springer Berlin Heidelberg

Download: atkey-2009-syntax.bib · atkey-2009-syntax.yml

Cites 18 works (2 here)

With notes (2)

Focusing on Binding and Computation licata-2008-focusingLICS · 2008

DOI

Higher-order abstract syntax pfenning-1988-higherPLDI · 1988

PDF · DOI · pldb

External (16)

Engineering formal metatheory (2008)
Parametric higher-order abstract syntax for mechanized semantics (2008)
Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism (2008)
Finally tagless, partially evaluated (2007)
Mechanizing metatheory in a logical framework (2007)
A foundation for embedded languages (2003)
Monadic encapsulation of effects: a revised approach (extended version) (2001)
The Theory of Parametricity in Lambda Cube (RIMS Kokyuroku 1217) (2001)
A new approach to abstract syntax involving binders (1999)
Semantical analysis of higher-order abstract syntax (1999)
Higher-Order Abstract Syntax in Coq (1995)
Metacircularity in the polymorphic λ-calculus (1991)
Constructions: A higher order proof system for mechanizing mathematics (1985)
Types, Abstraction and Parametric Polymorphism (1983)
Lambda-Definability in the Full Type Hierarchy (1980)
Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem (1972)