POPL 2017
Sun 15 - Sat 21 January 2017
Wed 18 Jan 2017 11:45 - 12:10 at Auditorium - Type Systems 1 Chair(s): Avik Chaudhuri

Reynolds’s Abstraction theorem forms the mathematical foundation for data abstraction. His setting was the polymorphic lambda calculus. Today, many modern languages, such as the ML family, employ rich module systems designed to give more expressive support for data abstraction than the polymorphic lambda calculus, but analogues of the Abstraction theorem for such module systems have lagged far behind.

We give an account of the Abstraction theorem for a modern module calculus supporting generative and applicative functors, higher-order functors, sealing, and translucent signatures. The main issues to be overcome are: (1) the fact that modules combine both types and terms, so they must be treated as both simultaneously, (2) the effect discipline that models the distinction between transparent and opaque modules, and (3) a very rich language of type constructors supporting singleton kinds. We define logical equivalence for modules and show that it coincides with contextual equivalence. This substantiates the folk theorem that modules are good for data abstraction. All our proofs are formalized in Coq.

Wed 18 Jan (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: POPL - Type Systems 1 at Auditorium
Chair(s): Avik ChaudhuriFacebook
POPL-2017-papers10:30 - 10:55
Stephen Dolan, Alan MycroftUniversity of Cambridge
POPL-2017-papers10:55 - 11:20
Radu GrigoreUniversity of Kent
POPL-2017-papers11:20 - 11:45
Cyrus OmarCarnegie Mellon University, Ian VoyseyCarnegie Mellon University, Michael HiltonOregon State University, USA, Jonathan AldrichCarnegie Mellon University, Matthew HammerUniversity of Colorado, Boulder
POPL-2017-papers11:45 - 12:10
Karl CraryCarnegie Mellon University