Andreas Rossberg
Max Planck Institute for Software Systems

Typed Open Programming -- A higher-order typed approach to dynamic modularity


Open programming -- the development of programs that support dynamic exchange of higher-order values and components -- is a domain currently dominated by untyped or weakly-typed languages. I present an approach for reconciling open programming with ML-style
strong static typing. 

I give a brief overview over the design of a concrete programming language, Alice ML, that extends Standard ML with a set of orthogonal features like higher-order modules, dynamic type checking, higher- order pickling, and concurrency. On top of these a flexible system of dynamic components and a simple but expressive notion of distribution is realised. The central concept in this design is the "package", a first-class value embedding a module along with its signature, which is dynamically checked whenever the module is extracted. 

The standard existential model of type abstraction is invalidated by the presence of primitives for dynamic type analysis. To maintain abstraction safety, I hence develop a calculus using dynamic generation of type names and a novel notion of "abstraction kinds" classifying abstract types. In order to recover ML-style after-the- fact type abstraction and type translucency, I further show how to extend the system with higher-order coercions over types and (dependent) kinds.

Host:  Bob Harper
Appointments:  April Foster <>

Friday, January 18, 2008
3:30 p.m.
Wean Hall 8220

Principles of Programming Seminars