Dependent types and program equivalence

Add to your list(s) Download to your calendar using vCal

• Stephanie Wierich, University of Pennsylvania
• Monday 02 November 2009, 12:45-14:00
• Room FW26, Computer Laboratory, William Gates Building.

If you have a question about this talk, please contact Sam Staton.

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 the term equivalence relation.

Almost all dependently-typed languages require this term equivalence 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, Omega, or Haskell, allow nonterminating computation, but do not allow those terms to appear in types. 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 total correctness properties. However, decidable type checking is not a prerequisite for type safety—and, in this context, type safety implies a weak form of correctness. Furthermore, decidability does not imply tractability. A decidable approximation of program equivalence may still not be useful in practice.

Therefore, we take a different approach: instead of a fixed, decidable, notion for term equivalence, we parameterize our type system with an abstract relation that is not necessarily decidable. We then design a novel set of typing rules that require only weak properties of this abstract relation in the proof of the preservation and progress lemmas. This design provides flexibility: we compare valid instantiations of term equivalence which range from beta-equivalence, to contextual equivalence, to some exotic equivalences.

This is joint work with Joint work with Limin Jia, Zianzhou Zhao, and Vilhelm Sjoberg.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Room FW26, Computer Laboratory, William Gates Building
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.