Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Thu 17 Jan 2019 09:44 - 10:06 at Sala I - Type Abstraction and Effects Chair(s): Benjamin Delaware

We give a translation suitable for compilation of modern module calculi supporting sealing, generativity, translucent signatures, applicative functors, higher-order functors and/or first-class modules. Ours is the first module-compilation translation with a dynamic correctness theorem. The theorem states that the translation produces target terms that are contextually equivalent to the source, in an appropriate sense. A corollary of the theorem is that the translation is fully abstract. Consequently, the translation preserves all abstraction present in the source. In passing, we also show that modules are a definitional extension of the underlying core language. All of our proofs are formalized in Coq.

Slides (talk.pdf)179KiB

Thu 17 Jan

Displayed time zone: Belfast change

09:00 - 10:06
Type Abstraction and EffectsResearch Papers at Sala I
Chair(s): Benjamin Delaware Purdue University
09:00
22m
Talk
Abstraction-Safe Effect Handlers via Tunneling
Research Papers
Yizhou Zhang Cornell University, Andrew C. Myers Cornell University
Link to publication DOI Media Attached
09:22
22m
Talk
Abstracting Algebraic Effects
Research Papers
Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław
Link to publication DOI Media Attached
09:44
22m
Talk
Fully Abstract Module Compilation
Research Papers
Karl Crary Carnegie Mellon University
Link to publication DOI Media Attached File Attached