Write a Blog >>
Wed 20 Jan 2016 15:35 - 16:00 at Grand Bay South - Track 2: Correct Compilation Chair(s): Jens Palsberg

Syntactic language extensions can introduce new facilities into a programming language while requiring little implementation effort and modest changes to the compiler. It is typical to desugar language extensions in a distinguished compiler phase after parsing or type checking, not affecting any of the later compiler phases. If desugaring happens before type checking, the desugaring cannot dependent on typing information and type errors are reported in terms of the generated code. If desugaring happens after type checking, the code generated by the desugaring is not type checked and may introduce vulnerabilities. Both options are undesirable.

We propose a system for syntactic extensibility where desugaring happens after type checking and desugarings are guaranteed to only generate well-typed code. A major novelty of our work is that desugarings operate on typing derivations instead of plain syntax trees. This provides desugarings access to typing information and forms the basis for the soundness guarantee we provide, namely that a desugaring generates a valid typing derivation. We have implemented our system for syntactic extensibility in a language-independent fashion and instantiated it for a substantial subset of Java, including generics and inheritance. We provide a sound Java extension for Scala-like for-comprehensions.

Paper Preprint (soundx-popl16.pdf)201KiB
Poster (SoundX poster.pdf)605KiB

Wed 20 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

14:20 - 16:00: Track 2: Correct CompilationResearch Papers at Grand Bay South
Chair(s): Jens PalsbergUniversity of California, Los Angeles
14:20 - 14:45
Fully-Abstract Compilation by Approximate Back-Translation
Research Papers
Dominique DevrieseiMinds - Distrinet, KU Leuven, Marco PatrignaniKU Leuven, Frank PiessensiMinds - Distrinet, KU Leuven
Pre-print Media Attached
14:45 - 15:10
Lightweight Verification of Separate Compilation
Research Papers
Jeehoon KangSeoul National University, Yoonseung KimSeoul National University (South Korea), Chung-Kil HurSeoul National University, Derek DreyerMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Media Attached File Attached
15:10 - 15:35
From MinX to MinC: Semantics-Driven Decompilation of Recursive Datatypes
Research Papers
Media Attached
15:35 - 16:00
Sound Type-dependent Syntactic Language Extension
Research Papers
Florian LorenzenTU Berlin, Sebastian ErdwegTU Darmstadt, Germany
Pre-print Media Attached File Attached