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

09:00 - 10:06: Research Papers - Type Abstraction and Effects at Sala I
Chair(s): Benjamin DelawarePurdue University
POPL-2019-Research-Papers09:00 - 09:22
Yizhou ZhangCornell University, Andrew MyersCornell University
Link to publication DOI Media Attached
POPL-2019-Research-Papers09:22 - 09:44
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
POPL-2019-Research-Papers09:44 - 10:06
Karl CraryCarnegie Mellon University
Link to publication DOI File Attached