Canonical typing and ∏-conversion in the Barendregt Cube

DOI10.1017/S0956796800001672MaRDI QIDQ4895552zbMATH OpenOpenAlexFDO

Authors Fairouz Kamareddine, Rob Nederpelt

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 systemstypabilitytype inference\(\Pi\)-conversionBarendregt cube

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• On -conversion in the -cube and the combination with abbreviations
• scientific article; zbMATH DE number 1499110
• The Barendregt cube with definitions and generalised reduction
• Pure type system conversion is always typable
• Typing in pure type systems

Cites work

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

Cited in

(6)

• Revisiting the notion of function
• A unified approach to type theory through a refined -calculus
• The soundness of explicit substitution with nameless variables
• A useful \(\lambda\)-notation
• On -conversion in the -cube and the combination with abbreviations
• Automath type inclusion in Barendregt's cube

This page was built for publication: Canonical typing and ∏-conversion in the Barendregt Cube

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