Canonical typing and ∏-conversion in the Barendregt Cube
Fairouz Kamareddine, Rob Nederpelt · Journal of Functional Programming · 1996
Abstract In this article, we extend the Barendregt Cube with ∏-conversion (which is the analogue of β-conversion, on product type level) and study its properties. We use this extension to separate the problem of whether a term is typable from the problem of what is the type of a term.