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...
| Published in: | ACM SIGPLAN Notices |
|---|---|
| Main Authors: | , , , |
| Format: | Article in Journal/Newspaper |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM)
2010
|
| Subjects: | |
| Online Access: | http://dx.doi.org/10.1145/1707801.1706333 https://dl.acm.org/doi/pdf/10.1145/1707801.1706333 |