| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 421863 | Electronic Notes in Theoretical Computer Science | 2011 | 15 Pages |
Abstract
We analyze a partial type checking algorithm for the inconsistent domain-free pure type system Type:Type (λ⁎). We show that the algorithm is sound and partially complete using a coinductive specification of algorithmic equality. This entails that the algorithm will only diverge due to the presence of diverging computations, in particular it will terminate for all typeable terms.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
