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 (6)

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

• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations