BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Closure Converting the Universes
DTSTART:20230428T140000
DTEND:20230428T153000
DTSTAMP:20260502T151902Z
UID:030fdf47d4da302d58bd759d09f400207afe15ec0be73052fe95e1d2
CATEGORIES:Conferences - Seminars
DESCRIPTION:Stefan Monnier\n Type preserving closure conversion of langua
 ges with dependent types has proved difficult.  It took until 2018 to ge
 t the first solution to the problem\, and that solution relies on language
  constructs custom-made for the purpose.  A first part of the problem is
  the fact that closure conversion inevitably requires some form of impredi
 cativity since a function can have free variables that belong to a higher 
 universe than itself\, but none of the existing forms of impredicativity (
 other than those known to be inconsistent) satisfy the needs of closure co
 nversion. A second part is that closure conversion exposes internal detail
 s of functions\, and those details affect the definitional equality of (co
 nverted) functions\, hence breaking type preservation. \n\nIn this paper 
 we propose to solve the first problem with the use of a new form of impred
 icativity\, and the second with a more restrictive notion of function equa
 lity.  This allows us to define a closure conversion that relies only on
  generic language constructs\, yet handles a dependently typed language wi
 th a tower of universes.
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR