ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Mon 12 Sep 2022 14:40 - 15:00 at Linhart - Analysis and Transformations Chair(s): Malgorzata Biernacka

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.

Mon 12 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

13:40 - 15:20
Analysis and TransformationsICFP Papers and Events at Linhart
Chair(s): Malgorzata Biernacka University of Wrocław
13:40
20m
Talk
Reference Counting with Frame Limited Reuse
ICFP Papers and Events
Anton Lorenzen University of Bonn, Daan Leijen Microsoft Research
DOI
14:00
20m
Talk
Entanglement Detection With Near-Zero CostDistinguished Paper
ICFP Papers and Events
Sam Westrick Carnegie Mellon University, Jatin Arora Carnegie Mellon University, Umut A. Acar Carnegie Mellon University
DOI
14:20
20m
Talk
Generating circuits with generators
ICFP Papers and Events
Marek Materzok University of Wroclaw
DOI
14:40
20m
Talk
Staged Compilation With Two-Level Type Theory
ICFP Papers and Events
András Kovács Eötvös Loránd University
DOI
15:00
20m
Talk
Random Testing of a Higher-Order Blockchain LanguageExperience Report
ICFP Papers and Events
Tram Hoang National University of Singapore, Anton Trunov Zilliqa Research, Leonidas Lampropoulos University of Maryland, College Park, Ilya Sergey National University of Singapore
DOI Pre-print