Tim Baanen


I am a PhD candidate at Vrije Universiteit Amsterdam, part of the Lean Forward project under the supervision of Jasmin Blanchette. My research interests lie are the intersection of computing science and mathematics, in a gradient from (intuitionistic) logic, type theory, formal verification to functional programming. Previously, I completed double majors in Computing Science and Mathematics at Utrecht University for my Bachelor and Master. During my time at Utrecht, I also wrote articles for the student newspaper de Vakidioot, was chair of the programming committee WebCie and am still a member of the LGBT+ organisation TrotCie. I am active in sustainable ecology, LGBT+ rights and software freedom.

Contact details

Legal Namedrs. T. (Tim) Baanen
AddressW&N Building, Room S-414
Vrije Universiteit Amsterdam
De Boelelaan 1081a
1081 HV Amsterdam
The Netherlands
Accept-languagenl, en;q=0.9, de;q=0.8, es;q=0.5, fr;q=0.4, "toki pona";q=0.1, Python, Haskell, Befunge, C, C++, Lean, assembly;q=0.4, Lisp;q=0.2, FORTH;q=0.2, *;q=0.1

Recent work

A predicate transformer semantics for effects
Wouter Swierstra and Tim Baanen. ICFP 2019.
Algebraic effects, specification and refinement
Tim Baanen, Master Thesis in Computing Science and Mathematics, Utrecht University. Supervisors: Wouter Swierstra and Jaap van Oosten.


I am an intuitionist.

The functional programmer sounds rather like a mediæval monk, denying himself the pleasures of life in the hope that it will make him virtuous.
John Hughes, Why Functional Programming Matters