BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Dependent types and program equivalence - Stephanie Wierich\, Univ
 ersity of Pennsylvania
DTSTART:20091102T124500Z
DTEND:20091102T140000Z
UID:TALK20701@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:The definition of type equivalence is one of the most importan
 t design issues\nfor any typed language. In dependently-typed languages\, 
 because terms appear\nin types\, this definition must rely on a definition
  of term equivalence.\nIn that case\, decidability of type checking requir
 es decidability for the\nterm equivalence relation.\n\nAlmost all dependen
 tly-typed languages require this term equivalence relation\nto be decidabl
 e. Some\, such as Coq\, Epigram or Agda\, do so by employing\nanalyses to 
 force all programs to terminate. Conversely\, others\, such as\nDML\, ATS\
 , Omega\, or Haskell\, allow nonterminating computation\, but do not\nallo
 w those terms to appear in types. In both cases\, decidable type checking\
 ncomes at a cost\, in terms of complexity and expressiveness.\n\nConversel
 y\, the benefits to be gained by decidable type checking are modest.\nTerm
 ination analyses allow dependently typed programs to verify total correctn
 ess\nproperties. However\, decidable type checking is not a prerequisite f
 or type\nsafety--and\, in this context\, type safety implies a weak form o
 f correctness.\nFurthermore\, decidability does not imply tractability. A 
 decidable approximation\nof program equivalence may still not be useful in
  practice.\n\nTherefore\, we take a different approach: instead of a fixed
 \, decidable\,\nnotion for term equivalence\, we parameterize our type sys
 tem with an abstract\nrelation that is not necessarily decidable. We then 
 design a novel set of\ntyping rules that require only weak properties of t
 his abstract relation\nin the proof of the preservation and progress lemma
 s. This design provides\nflexibility: we compare valid instantiations of t
 erm equivalence which range\nfrom beta-equivalence\, to contextual equival
 ence\, to some exotic equivalences.\n\nThis is joint work with Joint work 
 with Limin Jia\, Zianzhou Zhao\, and\nVilhelm Sjoberg.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR