POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 11:45 - 12:10 at Auditorium - Type Systems 3 Chair(s): Derek Dreyer

We present Turnstile, a metalanguage for creating typed embedded languages. To implement the type system, programmers write type checking rules resembling traditional judgment syntax. To implement the semantics, they incorporate elaborations into these rules. Turnstile critically depends on the idea of linguistic reuse. It exploits a macro system in a novel way to simultaneously type check and rewrite a surface program into a target language. Reusing a macro system also yields modular implementations whose rules may be mixed and matched to create other systems. Combined with compiler and runtime reuse, Turnstile produces performant typed languages with little effort.

Fri 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Type Systems 3POPL at Auditorium
Chair(s): Derek Dreyer MPI-SWS
10:30
25m
Talk
Intersection Type Calculi of Bounded Dimension
POPL
Andrej Dudenhefner Technical University Dortmund, Jakob Rehof Technical University Dortmund
10:55
25m
Talk
Type Soundness Proofs with Definitional Interpreters
POPL
Nada Amin EPFL, Tiark Rompf Purdue University
11:20
25m
Talk
Computational Higher-Dimensional Type Theory
POPL
Carlo Angiuli Carnegie Mellon University, Robert Harper , Todd Wilson California State University Fresno
11:45
25m
Talk
Type Systems as Macros
POPL
Stephen Chang Northeastern University, Alex Knauth Northeastern University, Ben Greenman Northeastern University