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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

09:00 - 10:06: Type Abstraction and EffectsResearch Papers at Sala I
Chair(s): Benjamin DelawarePurdue University
09:00 - 09:22
Abstraction-Safe Effect Handlers via Tunneling
Research Papers
Yizhou ZhangCornell University, Andrew C. MyersCornell University
Link to publication DOI Media Attached
09:22 - 09:44
Abstracting Algebraic Effects
Research Papers
Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław
Link to publication DOI Media Attached
09:44 - 10:06
Fully Abstract Module Compilation
Research Papers
Karl CraryCarnegie Mellon University
Link to publication DOI Media Attached File Attached