BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Éric Tanter (Universidad de Chile\, Chile)
DTSTART:20210520T170000Z
DTEND:20210520T180000Z
DTSTAMP:20260423T052448Z
UID:LoReL/5
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LoReL/5/">Gr
 adualizing the Calculus of Inductive Constructions</a>\nby Éric Tanter (U
 niversidad de Chile\, Chile) as part of LoReL Seminar\n\n\nAbstract\n(join
 t work with M. Bertrand\, K. Maillard\, N. Tabareau)\n\nAcknowledging the 
 ordeal of a fully formal development in a proof assistant such as Coq\, we
  investigate gradual variations on the Calculus of Inductive Construction 
 (CIC) for swifter prototyping with imprecise types and terms. We observe\,
  with a no-go theorem\, a crucial tradeoff between graduality and the key 
 properties of canonicity\, decidability and closure of universes under dep
 endent product that CIC enjoys. Beyond this Fire Triangle of Graduality\, 
 we explore the gradualization of CIC with three different compromises\, ea
 ch relaxing one edge of the Fire Triangle. We develop a parametrized prese
 ntation of Gradual CIC that encompasses all three variations\, and jointly
  develop their metatheory. We first present a bidirectional elaboration of
  Gradual CIC to a dependently-typed cast calculus\, which elucidates the i
 nterrelation between typing\, conversion\, and graduality. We then establi
 sh the metatheory of this cast calculus through both a syntactic model int
 o CIC\, which provides weak canonicity\, confluence\, and when applicable\
 , normalization\, and a monotone model that purports the study of the grad
 uality of two of the three variants. This work informs and paves the way t
 owards the development of malleable proof assistants and dependently-typed
  programming languages.\n\n[The talk will be on the “intro material” o
 f the paper\, namely the analysis that leads to the Fire Triangle\, and no
 t on the gory technical details of the metatheory of Gradual CIC]\n
LOCATION:https://researchseminars.org/talk/LoReL/5/
END:VEVENT
END:VCALENDAR