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.
Original language | English |
---|---|
Pages (from-to) | 245-267 |
Journal | Journal of Functional Programming |
Volume | 6 |
Issue number | 2 |
DOIs | |
Publication status | Published - 1996 |