A unified treatment of syntax with binders

DOI10.1017/S0956796812000251zbMath1252.68087MaRDI QIDQ3165528

François Pottier, Nicolas Pouillard

Publication date: 29 October 2012

Published in: Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

term representationsworld-polymorphic functions

Mathematics Subject Classification ID

Theory of programming languages (68N15) Data structures (68P05)

Uses Software

• Agda

Cites Work

• Telescopic mappings in typed lambda calculus
• External and internal syntax of the \(\lambda \)-calculus
• Substitution: A formal methods case study using monads and transformations
• A canonical locally named representation of binding
• First-order unification by structural recursion
• Alpha-structural recursion and induction
• Syntax for Free: Representing Syntax with Binding Using Parametricity
• de Bruijn notation as a nested datatype
• The Zipper
• The view from the left
• A fresh look at programming with names and binders
• Parametricity and dependent types
• Nameless, painless
• Binders unbound
• Applicative programming with effects
• An axiomatic basis for computer programming

This page was built for publication: A unified treatment of syntax with binders