Structural recursion with locally scoped names

DOI10.1017/S0956796811000116zbMath1271.68079MaRDI QIDQ3016213

Andrew M. Pitts

Publication date: 14 July 2011

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

Mathematics Subject Classification ID

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

Related Items

Normalization by evaluation and algebraic effects ⋮ Nominal lambda calculus: an internal language for FM-Cartesian closed categories ⋮ Denotational Semantics with Nominal Scott Domains ⋮ Propositions as sessions

Uses Software

• Freshml

Cites Work

• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Notions of computation and monads
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Nominal techniques in Isabelle/HOL
• The lambda-context calculus (extended version)
• Nominal unification
• Nominal logic, a first order theory of names and binding
• A universe of binding and computation
• Mechanizing the metatheory of LF
• A compiled implementation of strong reduction
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Alpha-structural recursion and induction
• Big-step normalisation
• Functions as processes
• A fresh look at programming with names and binders
• Nominal system T
• FreshML
• On equivalence and canonical forms in the LF type theory
• A proof theory for generic judgments
• Intensional interpretations of functionals of finite type I
• Primitive recursion for higher-order abstract syntax