Canonical typing and ∏-conversion in the Barendregt Cube

DOI10.1017/S0956796800001672zbMATH Open0854.03015OpenAlexW2153926566MaRDI QIDQ4895552FDOQ4895552

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

Recommendations

• On \(\Pi\)-conversion in the \(\lambda\)-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

zbMATH Keywords

type systemstypabilitytype inference\(\Pi\)-conversionBarendregt cube

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

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

Cited In (6)

• Revisiting the notion of function
• A unified approach to type theory through a refined \(\lambda\)-calculus
• The soundness of explicit substitution with nameless variables
• A useful \(\lambda\)-notation
• On \(\Pi\)-conversion in the \(\lambda\)-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)