Matthias Berg, Betreuer: Gert Smolka, Guido Tack
In an open programming system dynamic type checking is needed to safely link statically typed components. Since type case destroys the parametricity of type abstraction, dynamically generated type names are needed to hide the implementation of abstract types. Rossberg [2003] was the first to analyze the problem and to propose a calculus that solves it.
The goal of this Thesis is to greatly simplify Rossberg's calculus. We are looking for an extension of System F with type case and a binder for new type names. The calculus should have the unique type, the preservation, and the progress property, and these properties should be established by straightforward proofs. A model implementation of the calculus should be realized in Standard ML (with a de Bruijn implementation of variables).
A major simplification of Rossberg's calculus seems possible since his coercions are not needed. The idea is to have a global environment for dynamically generated type names and to formulate the reduction rules with evaluation contexts. For terms without type case, a bisimulation with pure system F should exist. In a second step, the calculus should be extended with deterministic by need-futures (see [Niehren et al 2004] for concurrent by need-futures) so that lazy linking can be expressed [Rossberg 2004].
Finally, the calculus should be extended to F_omega or even the lambda cube. Proofs of the safety properties are probably too difficult, but a model implementation should be given. Rossberg's [2004] component model should provide interesting examples.
Sumii and Pierce [2004] consider abstract types in a setting without static types. They also use dynamically generated names. Exploring the relationship to Rossberg's approach should be interesting.
Andreas Rossberg, Generativity and Dynamic Opacity for Abstract Types. Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Uppsala, Sweden, ACM Press 2003.
Andreas Rossberg, What are Components? Slides, March 2004.
Joachim Niehren, Jan Schwinghammer, Gert Smolka. A Concurrent Lambda Calculus with Futures. Technical Report, Programming Systems Lab, 2004.
Eijiro Sumii and Benjamin C. Pierce, A bisimulation for dynamic sealing. Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of programming languages. ACM Press, January 2004.