BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Cancelled : Full reduction in the face of absurdity. - Didier Remy
  - Inria
DTSTART:20150520T130000Z
DTEND:20150520T140000Z
UID:TALK58955@talks.cam.ac.uk
CONTACT:David Greaves
DESCRIPTION:<b>Note: Talk cancelled for today - speaker cannot make it.</b
 >\n\n\n  Adding GADTs to a language such as ML or System F in\ntroduces lo
 gical   assumptions in the type system\, which breaks type soundness in th
 e   presence of full reduction.  Even though programming languages use wea
 k\nreduction strategies\, typically call-by-value\, we believe that type  
  soundness for full reduction in the underlying effect-free core calculus\
 n  is important and gives the programmer a more abstract understanding of\
 n  program fragments.  We propose an expressive type system with implicit\
 n  coercions and both coherent and incoherent abstraction over\n  coercion
 s. This allows a fine-grained control of dependencies between\n  computati
 ons and the logical hypotheses they depend on while preserving\n  the impl
 icit use of hypotheses and confluence. Combining implicit\n  hypotheses an
 d full reduction leads to a better understanding of GADTs\, provides a bet
 ter continuum between explicit and implicit type\n  information\, and woul
 d be a good setting for studying extraction of\n  computational contents f
 rom proofs in proof assistants.
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR