Dependent types and program equivalence

10 years 6 months ago
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 term equivalence relation. Almost all dependently-typed languages require this relation to be decidable. Some, such as Coq, Epigram or Agda, do so by employing analyses to force all programs to terminate. Conversely, others, such as DML, ATS, mega, or Haskell, allow nonterminating computation, but do not allow those terms to appear in types. Instead, they identify a terminating index language and use singleton types to connect indices to computation. In both cases, decidable type checking comes at a cost, in terms of complexity and expressiveness. Conversely, the benefits to be gained by decidable type checking are modest. Termination analyses allow dependently typed programs to verify tot...
Jianzhou Zhao, Limin Jia, Stephanie Weirich, Vilhe
Added 01 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where POPL
Authors Jianzhou Zhao, Limin Jia, Stephanie Weirich, Vilhelm Sjöberg
Comments (0)