Syntax for Free: Representing Syntax with Binding Using Parametricity

DOI10.1007/978-3-642-02273-9_5zbMath1246.68084OpenAlexW1560964942MaRDI QIDQ3637185

Robert Atkey

Publication date: 7 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://strathprints.strath.ac.uk/34483/

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (2)

A unified treatment of syntax with binders ⋮ Incorporating quotation and evaluation into Church's type theory

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Metacircularity in the polymorphic \(\lambda\)-calculus
• Monadic encapsulation of effects: a revised approach (extended version)
• Engineering formal metatheory
• Parametric higher-order abstract syntax for mechanized semantics
• Mechanizing metatheory in a logical framework
• Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism

This page was built for publication: Syntax for Free: Representing Syntax with Binding Using Parametricity