# Bachelor Thesis: Polymorphic Lambda Calculus with Dynamic Types

Matthias Berg,
Betreuer: Gert Smolka,
Guido Tack

## Motivation

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.

## Task Formulation

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.

## Related Work

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.

## Bibliography

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.

## Documents

Thesis (postscript)

Thesis (pdf)

Task formulation (slides)

Final Presentation (slides)