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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Fri 20 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:10 | |||
10:30 25mTalk | Intersection Type Calculi of Bounded Dimension POPL | ||
10:55 25mTalk | Type Soundness Proofs with Definitional Interpreters POPL | ||
11:20 25mTalk | Computational Higher-Dimensional Type Theory POPL Carlo Angiuli Carnegie Mellon University, Robert Harper , Todd Wilson California State University Fresno | ||
11:45 25mTalk | Type Systems as Macros POPL Stephen Chang Northeastern University, Alex Knauth Northeastern University, Ben Greenman Northeastern University |