A useful -notation

DOI10.1016/0304-3975(95)00101-8MaRDI QIDQ1365680zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 4048997 (Why is no real title available?)
• scientific article; zbMATH DE number 4058907 (Why is no real title available?)
• scientific article; zbMATH DE number 3659007 (Why is no real title available?)
• scientific article; zbMATH DE number 108365 (Why is no real title available?)
• A unified approach to type theory through a refined -calculus
• Canonical typing and ∏-conversion in the Barendregt Cube
• Explicit substitutions
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• ON STEPWISE EXPLICIT SUBSTITUTION
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• The Barendregt cube with definitions and generalised reduction

Cited in

(18)

• Characteristics of de Bruijn’s early proof checker Automath
• Explicit substitutions à la de Bruijn: the local and global way
• Revisiting the notion of function
• A flexible framework for visualisation of computational properties of general explicit substitutions calculi
• Canonical typing and ∏-conversion in the Barendregt Cube
• A unified approach to type theory through a refined -calculus
• A notation for lambda terms. A generalization of environments
• The soundness of explicit substitution with nameless variables
• Important Issues in Foundational Formalisms
• 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
• Automath and Pure Type Systems
• 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

Describes a project that uses

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)