BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Staged Compilation with Two-Level Type Theory - András Kovács\, 
 Eötvös Loránd University
DTSTART:20220822T130000Z
DTEND:20220822T140000Z
UID:TALK177878@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:The aim of staged compilation is to enable metaprogramming in 
 a way such that we have guarantees about the well-formedness of code outpu
 t\, and we can also mix together object-level and meta-level code in a con
 cise and convenient manner. In this work\, we observe that two-level type 
 theory (2LTT)\, a system originally devised for the purpose of developing 
 synthetic homotopy theory\, also serves as a system for staged compilation
  with dependent types. 2LTT has numerous good properties for this use case
 : it has a concise specification\, well-behaved model theory\, and it supp
 orts a wide range of language features both at the object and the meta lev
 el. First\, we give an overview of 2LTT’s features and applications in s
 taging. Then\, we present a staging algorithm and prove its correctness. O
 ur algorithm is ``staging-by-evaluation’’\, analogously to the techniq
 ue of normalization-by-evaluation\, in that staging is given by the evalua
 tion of 2LTT syntax in a semantic domain. The staging algorithm together w
 ith its correctness constitutes a proof of strong conservativity of 2LLT o
 ver the object theory. To our knowledge\, this is the first description of
  staged compilation which supports full dependent types and unrestricted s
 taging for types.
LOCATION:FW11
END:VEVENT
END:VCALENDAR