Staged Compilation with Two-Level Type Theory

Add to your list(s) Download to your calendar using vCal

• András Kovács, Eötvös Loránd University
• Monday 22 August 2022, 14:00-15:00
• FW11.

If you have a question about this talk, please contact Jamie Vicary.

This talk has been canceled/deleted

The aim of staged compilation is to enable metaprogramming in a way such that we have guarantees about the well-formedness of code output, and we can also mix together object-level and meta-level code in a concise 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 supports a wide range of language features both at the object and the meta level. First, we give an overview of 2LTT’s features and applications in staging. Then, we present a staging algorithm and prove its correctness. Our algorithm is ``staging-by-evaluation’’, analogously to the technique of normalization-by-evaluation, in that staging is given by the evaluation of 2LTT syntax in a semantic domain. The staging algorithm together with its correctness constitutes a proof of strong conservativity of 2LLT over the object theory. To our knowledge, this is the first description of staged compilation which supports full dependent types and unrestricted staging for types.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

This talk is not included in any other list

Note that ex-directory lists are not shown.