ON STEPWISE EXPLICIT SUBSTITUTION

DOI10.1142/S0129054193000146MaRDI QIDQ4286110zbMATH OpenFDO

Authors Fairouz Kamareddine, Rob Nederpelt

Publication date 27 April 1994

Published in International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1142/S0129054193000146

zbMATH Keywords

substitutionlambda calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 1424037
• Explicit substitutions
• scientific article; zbMATH DE number 1722651
• A Theory of Explicit Substitutions with Safe and Full Composition
• A useful -notation

Cited in

(16)

• On explicit substitutions and names (extended abstract)
• Explicit substitutions à la de Bruijn: the local and global way
• 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
• scientific article; zbMATH DE number 1722651 (Why is no real title available?)
• A note on complexity measures for inductive classes in constructive type theory
• scientific article; zbMATH DE number 1424037 (Why is no real title available?)
• λν, a calculus of explicit substitutions which preserves strong normalisation
• The soundness of explicit substitution with nameless variables
• A useful -notation
• Explicit substitution. On the edge of strong normalization
• On explicit substitution with names
• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Comparing calculi of explicit substitutions with eta-reduction
• Refining reduction in the lambda calculus

This page was built for publication: ON STEPWISE EXPLICIT SUBSTITUTION

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