A useful \(\lambda\)-notation
From MaRDI portal
Publication:1365680
DOI10.1016/0304-3975(95)00101-8zbMath0873.03018OpenAlexW2155411851MaRDI QIDQ1365680
Fairouz Kamareddine, Rob Nederpelt
Publication date: 9 September 1997
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(95)00101-8
Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Combinatory logic and lambda calculus (03B40)
Related Items
A unified approach to type theory through a refined \(\lambda\)-calculus ⋮ Strong normalization from weak normalization in typed \(\lambda\)-calculi ⋮ Characteristics of de Bruijn’s early proof checker Automath ⋮ Revisiting the notion of function ⋮ Canonical typing and ∏-conversion in the Barendregt Cube ⋮ Comparing Calculi of Explicit Substitutions with Eta-reduction ⋮ De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case ⋮ Automath and Pure Type Systems ⋮ Explicit Substitutions à la de Bruijn ⋮ De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case ⋮ A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi ⋮ Comparing and implementing calculi of explicit substitutions with eta-reduction ⋮ SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi ★ ⋮ THE SOUNDNESS OF EXPLICIT SUBSTITUTION WITH NAMELESS VARIABLES
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
- A unified approach to type theory through a refined \(\lambda\)-calculus
- The Barendregt cube with definitions and generalised reduction
- ON STEPWISE EXPLICIT SUBSTITUTION
- Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
- Canonical typing and ∏-conversion in the Barendregt Cube
- Explicit substitutions
