Revisiting the notion of function

DOI10.1016/S1567-8326(02)00016-4zbMath1020.03013MaRDI QIDQ1394989

Twan Laan, Fairouz Kamareddine, Rob Nederpelt

Publication date: 25 June 2003

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

zbMATH Keywords

\(\lambda\)-calculusexplicit substitutionAutomathinstantiation\(\Pi\)-reductionBarendregt cubefunction abstractionfunctionalisation

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Automath and Pure Type Systems

Uses Software

• ML
• Automath

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The calculus of constructions
• Strictness analysis via abstract interpretation for recursively defined types
• On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• A useful \(\lambda\)-notation
• A set of postulates for the foundation of logic. II
• The Barendregt cube with definitions and generalised reduction
• Pure type systems with explicit substitution
• λν, a calculus of explicit substitutions which preserves strong normalisation
• Constructive natural deduction and its ‘ω-set’ interpretation
• Canonical typing and ∏-conversion in the Barendregt Cube
• Explicit substitutions