Dependent types and Program Equivalence
The definition of type equivalence is one of the most important design issues for any typed language. In dependently-typed 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 th...
| Main Authors: | , , , |
|---|---|
| Format: | Conference Object |
| Language: | unknown |
| Published: |
2010
|
| Subjects: | |
| Online Access: | https://repository.upenn.edu/handle/20.500.14332/6698 https://hdl.handle.net/20.500.14332/6698 |