DRAFT—Do not distribute Dependent Types and Program Equivalence
The definition of type equivalence is one of the most important design issues for any typed language. In dependentlytyped languages, because terms appear in types, this definition must rely on a definition of term equivalence. In that case, decidability of type checking requires decidability for the...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Subjects: | |
| Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.409.5359 http://www.andrew.cmu.edu/user/liminjia/research/papers/lambda-eek.pdf |