The lambda-context calculus (extended version)
From MaRDI portal
Publication:1044184
DOI10.1016/J.IC.2009.06.004zbMath1192.68137OpenAlexW2088018993MaRDI 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
functional programmingexplicit substitutionslambda-calculusnominal techniquesbinderscalculi of contextscapturing substitution
Related Items (3)
Structural recursion with locally scoped names ⋮ Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms ⋮ PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
Cites Work
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: The lambda-context calculus (extended version)
