BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Semantics Lunch (Computer Laboratory)
SUMMARY:Dependent types and program equivalence - Stephani
e Wierich\, University of Pennsylvania
DTSTART;TZID=Europe/London:20091102T124500
DTEND;TZID=Europe/London:20091102T140000
UID:TALK20701AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/20701
DESCRIPTION:The definition of type equivalence is one of the m
ost important design issues\nfor any typed languag
e. In dependently-typed languages\, because terms
appear\nin types\, this definition must rely on a
definition of term equivalence.\nIn that case\, de
cidability of type checking requires decidability
for the\nterm equivalence relation.\n\nAlmost all
dependently-typed languages require this term equi
valence relation\nto be decidable. Some\, such as
Coq\, Epigram or Agda\, do so by employing\nanalys
es to force all programs to terminate. Conversely\
, others\, such as\nDML\, ATS\, Omega\, or Haskell
\, allow nonterminating computation\, but do not\n
allow those terms to appear in types. In both case
s\, decidable type checking\ncomes at a cost\, in
terms of complexity and expressiveness.\n\nConvers
ely\, the benefits to be gained by decidable type
checking are modest.\nTermination analyses allow d
ependently typed programs to verify total correctn
ess\nproperties. However\, decidable type checking
is not a prerequisite for type\nsafety--and\, in
this context\, type safety implies a weak form of
correctness.\nFurthermore\, decidability does not
imply tractability. A decidable approximation\nof
program equivalence may still not be useful in pra
ctice.\n\nTherefore\, we take a different approach
: instead of a fixed\, decidable\,\nnotion for ter
m equivalence\, we parameterize our type system wi
th an abstract\nrelation that is not necessarily d
ecidable. We then design a novel set of\ntyping ru
les that require only weak properties of this abst
ract relation\nin the proof of the preservation an
d progress lemmas. This design provides\nflexibili
ty: we compare valid instantiations of term equiva
lence which range\nfrom beta-equivalence\, to cont
extual equivalence\, to some exotic equivalences.\
n\nThis is joint work with Joint work with Limin J
ia\, Zianzhou Zhao\, and\nVilhelm Sjoberg.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Bu
ilding
CONTACT:Sam Staton
END:VEVENT
END:VCALENDAR