The lambda-context calculus (extended version)

DOI10.1016/j.ic.2009.06.004zbMath1192.68137MaRDI QIDQ1044184

Stéphane Lengrand, Murdoch James Gabbay

Publication date: 11 December 2009

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2009.06.004

zbMATH Keywords

functional programming; explicit substitutions; lambda-calculus; nominal techniques; binders; calculi of contexts; capturing substitution

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

Related Items

PNL to HOL: from the logic of nominal sets to the logic of higher-order functions, Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms, Structural recursion with locally scoped names

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Notions of computation and monads
• Capture-avoiding substitution as a nominal algebra
• A lambda-calculus for dynamic binding
• A calculus of mobile processes. II
• Nominal unification
• Nominal rewriting
• Enriching the lambda calculus with contexts
• Nominal Equational Logic
• Modal Foundations for Predicate Logic
• One-and-a-Halfth Order Terms: Curry-Howard and Incomplete Derivations
• A Nominal Axiomatization of the Lambda Calculus
• A Formal Calculus for Informal Equality with Binding
• Nominal (Universal) Algebra: Equational Logic with Names and Binding
• Term Rewriting and All That
• Two-level Lambda-calculus
• Computer Science Logic
• Programming Languages and Systems
• Foundations of Software Science and Computational Structures
• Parallel reductions in \(\lambda\)-calculus
• A calculus of lambda calculus contexts
• A typed context calculus