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 |
| Published: |
2009
|
| Subjects: | |
| Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.163.6638 http://www.andrew.cmu.edu/user/liminjia/research/papers/lambdaEq.pdf |