[Pl-seminar] *Friday* 6/10: Claudio Russo, "F-ing Modules"

[Aaron Turon]

NEU Programming Languages Seminar presents

Claudio Russo
Microsoft Research, Cambridge

*Friday* 6/10
11:45am - 1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

F-ing Modules
(with Andreas Rossberg (Google) and Derek Dreyer (MPI-SWS))

ML modules are a powerful language mechanism for decomposing programs
into reusable components. They also have a reputation for being
complex, and dependent on fancy type theory that is mostly opaque to
non-experts.

While this reputation is certainly understandable, we aim to show that
it is undeserved. After an introduction to modules, I'll present our
dead simple elaboration semantics for a full-featured, higher-order
ML-like module language. Our elaboration defines the meaning of module
expressions by a straightforward, compositional translation into
vanilla System F (the polymorphic lambda-calculus), under plain F
typing contexts. We thereby show that modules are merely a particular
mode of use of System F.

Our module language supports the usual second-class modules, with
SML-style generative functors and local modules. To demonstrate the
versatility of our approach, I’ll further extend the language with the
ability to package modules as first-class values -- an almost trivial
extension, as it turns out.

This work was presented at TLDI'2010 and has been formalized in Coq.