Anne 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

Full Namedrs. T. (Anne) Baanen
AddressNieuwe Universiteitsgebouw, room 12A-77 (east wing, 12th floor)
Vrije Universiteit Amsterdam
De Boelelaan
1111 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 Lean tactic for normalising ring expressions with exponents (short paper) (preprint version)
Anne Baanen. IJCAR 2020.
Combining predicate transformer semantics for effects: a case study in parsing regular languages
Anne Baanen and Wouter Swierstra. MSFP 2020.
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.

In a previous version of this paper we offered an invariant for proving the correctness of this incorrect variation on the mutator. We did, however, not include the proof!
Jan L.A. van de Snepscheut, "Algorithms for on-the-fly-garbage collection' revisited, Information Processing Letters 24:4, 1987.