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: | Text |
Language: | unknown |
Published: |
ScholarlyCommons
2010
|
Subjects: | |
Online Access: | https://repository.upenn.edu/cis_papers/632 https://repository.upenn.edu/cgi/viewcontent.cgi?article=1668&context=cis_papers |