A BRICS Mini-Course
April 9-11, 2003
Lectures by
Steffen van Bakel, svb@doc.ic.ac.uk
Department of Computing, Imperial College, London, UK
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.
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.
At the end of the notes there is an extensive list of papers. The notes themselves are based on (mainly) two papers: