A useful -notation

DOI10.1016/0304-3975(95)00101-8zbMATH Open0873.03018OpenAlexW2155411851MaRDI QIDQ1365680FDOQ1365680

Authors: 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

Recommendations

• Refining reduction in the lambda calculus
• scientific article; zbMATH DE number 1332647
• A notation for lambda terms. A generalization of environments
• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
• ON STEPWISE EXPLICIT SUBSTITUTION

zbMATH Keywords

\(\lambda\)-calculuscanonical typeitem notationpreference typereduction relation

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Cites Work

• Title not available (Why is that?)
• Explicit substitutions
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Title not available (Why is that?)
• A unified approach to type theory through a refined \(\lambda\)-calculus
• Title not available (Why is that?)
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• Title not available (Why is that?)
• The Barendregt cube with definitions and generalised reduction
• ON STEPWISE EXPLICIT SUBSTITUTION
• Canonical typing and ∏-conversion in the Barendregt Cube

Cited In (18)

• Characteristics of de Bruijn’s early proof checker Automath
• Explicit substitutions à la de Bruijn: the local and global way
• A flexible framework for visualisation of computational properties of general explicit substitutions calculi
• Revisiting the notion of function
• Canonical typing and ∏-conversion in the Barendregt Cube
• A unified approach to type theory through a refined \(\lambda\)-calculus
• The soundness of explicit substitution with nameless variables
• A notation for lambda terms. A generalization of environments
• Important Issues in Foundational Formalisms
• Automath and Pure Type Systems
• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case
• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
• Reviewing the classical and the de Bruijn notation for \(\lambda\)-calculus and pure type systems
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Comparing calculi of explicit substitutions with eta-reduction
• ON STEPWISE EXPLICIT SUBSTITUTION
• SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi

Uses Software

• Automath

This page was built for publication: A useful \(\lambda\)-notation

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