Structural recursion with locally scoped names

DOI10.1017/S0956796811000116MaRDI QIDQ3016213zbMATH OpenFDO

Authors Andrew M. Pitts

Publication date 14 July 2011

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

Full work available at URL https://doi.org/10.1017/S0956796811000116

Mathematics Subject Classification ID

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

Recommendations

• Relating two semantics of locally scoped names
• Using Structural Recursion for Corecursion
• Structures for structural recursion
• scientific article; zbMATH DE number 3963179
• Computational soundness of a call by name calculus of recursively-scoped records
• Recursive and dynamic structures in generic programming
• scientific article; zbMATH DE number 4049007
• A hierarchy for delimited continuations in call-by-name
• scientific article; zbMATH DE number 1390021
• scientific article; zbMATH DE number 1948183

Cites work

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

Cited in

(5)

• Normalization by evaluation and algebraic effects
• Nominal lambda calculus: an internal language for FM-Cartesian closed categories
• Propositions as sessions
• Relating two semantics of locally scoped names
• Denotational semantics with nominal Scott domains

Describes a project that uses

Uses Software

• FreshML

This page was built for publication: Structural recursion with locally scoped names

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3016213)