On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations

DOI10.1016/S0168-0072(98)00019-0zbMath0930.03012OpenAlexW2062081760MaRDI QIDQ1302298

Rob Nederpelt, Fairouz Kamareddine, Roel Bloo

Publication date: 15 February 2000

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0168-0072(98)00019-0

zbMATH Keywords

normalizationtyped \(\lambda\)-calculus\(\lambda\)-cube\(\Pi\)-conversion\(\Pi\)-reductionabbreviationsabstraction operatorssubject-reduction

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Automath Type Inclusion in Barendregt’s Cube, Revisiting the notion of function, De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: The typed case, Automath and Pure Type Systems, Unnamed Item, A Framework for Defining Logical Frameworks

Uses Software

• Coq
• Automath
• LEGO
• TIL

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• The Barendregt cube with definitions and generalised reduction
• Refining reduction in the lambda calculus
• Canonical typing and ∏-conversion in the Barendregt Cube
• Unnamed Item
• Unnamed Item