Canonical typing and ∏-conversion in the Barendregt Cube

DOI10.1017/S0956796800001672zbMath0854.03015OpenAlexW2153926566MaRDI QIDQ4895552

Rob Nederpelt, Fairouz Kamareddine

Publication date: 17 November 1996

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796800001672

zbMATH Keywords

type systemstype inferencetypability\(\Pi\)-conversionBarendregt cube

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

A unified approach to type theory through a refined \(\lambda\)-calculus, A useful \(\lambda\)-notation, Automath Type Inclusion in Barendregt’s Cube, Revisiting the notion of function, THE SOUNDNESS OF EXPLICIT SUBSTITUTION WITH NAMELESS VARIABLES, On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations

Cites Work

• A unified approach to type theory through a refined \(\lambda\)-calculus
• A useful \(\lambda\)-notation
• A set of postulates for the foundation of logic
• ON STEPWISE EXPLICIT SUBSTITUTION
• Refining reduction in the lambda calculus
• A formulation of the simple theory of types