BRICS · Contents · Lecturer · Programme · References

Semantics with Intersection Types

A BRICS Mini-Course
April 9-11, 2003

Lectures by
Steffen van Bakel,
Department of Computing, Imperial College, London, UK

Course Contents

The course will introduce intersection type assignment for the Lambda Calculus, define a notion of approximant for terms, and show the relation between assignable types and approximants for terms. Using this result, (head/strong) normalisation is easily characterised.

A filter semantics for the LC will be defined, that will be shown sound and complete.

The second half of the course will be dedicated to intersection type assignment for Combinator Systems and Term Rewriting Systems, and we will show that (part of) the results for the LC can be shown to hold here as well.

About the Lecturer

I joined the Imperial College as a Lecturer in January 1996. Prior to my arrival I was working as post-doc at the Department of Computer Science of the University of Turin, Italy, from March 1993. Before that, I held a research position at the group of Functional Languages of the University of Nijmegen, the Netherlands.

My MSc (doctoraal, 1988) in Computer Science and PhD (1993) in Mathematics and Computer Science were obtained at the University of Nijmegen.

I currently work in the field of Type Assignment both for Lambda Calculus and Term Rewriting Systems, an area that I explored first in my PhD-thesis, and I have since then investigated further, mostly in collaboration with M. Fernández from École Normale Supérieure, Paris. My specialisation in that area is that of Intersection Type Assignment.


Wednesday April 9, 2003, 15:15-17:00 in Auditorium D4

Thursday April 10, 2003, 15:15-17:00 in Auditorium D4

Friday April 11, 2003, 15:15-17:00 in Auditorium D4


The lecture notes of the mini course are available at svb/SemIntTypes.

At the end of the notes there is an extensive list of papers. The notes themselves are based on (mainly) two papers: