Copenhagen Programming Language Seminar


Type-Based Termination
A polymorphic lambda-calculus with sized higher-order types

Andreas Abel,
Theoretical Computer Science, University of Munich

Friday (!), March 9th, Time: 11:00 - 12:00 (!)
IT University of Copenhagen, Rued Langgaards Vej 7, Auditorium 4


Semantically, one can define terminating recursive functions by induction on ordinals. Type-Based Termination turns this insight into a typing rule for the fixed-point combinator. The marriage of termination and type checking is especially fruitful in the analysis of higher-order functional programs which might even involve higher-rank polymorphism. On the contrary, traditional syntax-based approaches developed for term rewriting systems and first-order functional programs do not handle higher-order features well.

In this talk, I will present my doctoral thesis: Type-based termination for the higher-order polymorphic lambda-calculus (F^omega), which is the basis for the functional language Haskell.

Scientific host: Carsten SchŘermann. Administrative host: Camilla Torp-Smith. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL.
COPLAS is sponsored by FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org