Steffen van Bakel
(IPA: Stɛffən vɑn Ba:kəl)
|
|
|
Senior Lecturer
Deputy Examinations Officer
|
|
|
|
|
|
|
180 Queen's Gate, London SW7 2BZ, UK
|
|
|
(λxy.svbximperialyacyuk)@.
|
|
(+44) (0)20 7594 8263
|
|
Fax:
|
(+44) (0)20 7594 8932
|
I joined the Group of Theory & Formal Methods (now called Programming Languages and Systems) in the Department of Computing at Imperial College London as a Lecturer in January 1996.
Prior to my arrival I was working as post-doc in the group of Semantics and Logics of Computation at the Department of Computer Science of the University of Turin, Piemonte, Italy, from March 1993. Before that, I held a research position at the group of Functional Languages (now Software Technology), at the Computing Science Institute 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. My thesis supervisors (promotores) were M. Dezani-Ciancaglini from Turin and H. Barendregt from Nijmegen.
And yes, that makes me an immigrant.
My main research lies 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. My specialisation in that area is that of Intersection Type Assignment.
More recently, I started working in the area of Mobile Ambients, Object Orientation, and that of Systems Biology.
My main topic of research over the last years is that of the relation between Classical Logic and Computation, and I have, together with Stefano Berardi, organised a number of workshops on that topic.
My interest is mainly semantical, and I have studied the (im)possiblility of intersection type assignment and filter semantics for a number of calculi.
I have also studied semantic mappings of classical calculi into the π-calculus, which has led to output-based encodings of the λ-calculus and the λμ-calculus, as well as for X.
- I have been the thesis supervisor for Elham Kashefi, Alexander J. Summers (who in January 2015 was awarded the Junior Dahl Nygaard prize for his work on the verification of object-oriented programs and type systems), Jayshan Raghunandan, Reuben N.S. Rowe, and Rabih Mohsen.
- In the autumn term, I teach Type Systems for Programming Languages (course 60023), an introductory course on my own research area.
- In the autumn term, I teach the first part of Discrete Maths, Logic, and Reasoning (course 40018A).
- In December 2002 and April 2003, while visiting ENS Lyon, France, and BRICS Aarhus, Denmark, respectivley, I taught Semantics with Intersection Types, a course on my own research area.
Research interest
- Functional Programming:
- Lambda Calculus.
- Term Rewriting Systems.
- Term Graph Rewriting Systems.
- Mobile Ambients.
- Type systems:
- Sequent Calculus for Classical Logic.
- Curry Howard Isomorphism.
- Intersection type assignment.
- Polymorphic type assignment.
- Decidable systems.
- Type theory and theorem provers.
- Semantics:
- Filter models.
- Approximation models.
- Game theory.
- Abstract interpretation.
Click here for a complete list of my publications, and here if you want to find out how to make bibtex respect Dutch sorting of family names.
In case you would like to use my macros for derivation construction in LaTeX (built on top of Paul Taylor's prooftrees), you can download derivation.sty (or derivation-nops.sty if you do not like using pstricks).
