About

I recently obtained my PhD at Vrije Universiteit Amsterdam, as part of the Lean Forward project under the supervision of Jasmin Blanchette and Sander Dahmen. My research interests lie in 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. I am active in sustainable ecology, LGBT+ rights and software freedom.

Contact details

Full Name	dr. A. (Anne) Baanen
E-mail	anne@anne.mx
Pronouns	they/them
Accept-language	nl, en;q=0.9, es;q=0.8, de;q=0.7, fr;q=0.4, Lean, Python, Haskell, Befunge, C, C++, assembly;q=0.6, Lisp;q=0.6, Rust;q=0.5, FORTH;q=0.2, *;q=0.1

Recent work

Lean Formalization of Completeness Proof for Coalition Logic with Common Knowledge

Kai Obendrauf, Anne Baanen, Patrick Koopmann and Vera Stebletsova, ITP 2024.

Formalizing fundamental algebraic number theory

Anne Baanen, PhD thesis in theoretical computer science. Supervisors: Jasmin Blanchette and Sander R. Dahmen. Defence 2024-01-29. Slides.

Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves

Anne Baanen, Alex J. Best, Nirvana Coppola and Sander R. Dahmen. CPP 2023.
Previous versions available in the arXiv.

A formalization of Dedekind domains and class groups of global fields

Anne Baanen, Sander R. Dahmen, Ashvni Narayanan and Filippo A. E. Nuccio. Journal of Automated Reasoning 66, 611–637 (2022).
Extended version of a paper presented at ITP 2021.
Previous versions available in the arXiv.

(Original version) A formalization of Dedekind domains and class groups of global fields

Anne Baanen, Sander R. Dahmen, Ashvni Narayanan and Filippo A. E. Nuccio. ITP 2021.
Previous versions available in the arXiv.

Use and abuse of instance parameters in the Lean mathematical library

Anne Baanen. ITP 2022.
Previous versions available in the arXiv.

A Lean tactic for normalising ring expressions with exponents (short paper)

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.

Talks and workshops

2024-05-28: Presented tutorial on structures and classes in Lean, Formalisation of Mathematics: Workshop for Women and Mathematicians of Minority Gender, ICMS, Edinburgh, Scotland.
2023-07-12: Presented tutorial on structures and algebra in Lean, Machine-checked Mathematics, Lorentz Center, Leiden, Netherlands.
2023-05: Co-organized Formalization of Cohomology Theories, BIRS, Banff, Canada.
2023-02-14: Presented Computing with or despite the computer at Machine Assisted Proofs 2023, IPAM, UCLA, Los Angeles, United States of America.
Slides; Recording
2022-09-24: Presented Bundling in dependent type theory at EPN WG-4 Workshop, CLAS 2022, Tbilisi, Georgia.
Slides
2022-08-23: Assisted Johan Commelin at Hands on with Lean at GQT graduate school 2022, Zeist, Netherlands.
2022-08-10: Presented Use and abuse of instance parameters in the Lean mathematical library at ITP 2021, Haifa, Israel.
Paper; Slides
2022-06-03: Presented Introduction to formalizing number theory at the ICNT seminar, Amsterdam, Netherlands.
Slides
2022-03-04: Presented Type classes for morphisms and substructures at Machine-Checked-Mathematics, Leiden, Netherlands Online.
Demo file
2021-06-29: Presented A formalization of Dedekind domains and class groups of global fields at ITP 2021, Rome, Italy Online.
Paper; Slides; Recording
2020-07-16: Presented Linear algebra in mathlib at LFTCM 2020, Online.
Slides; Recording
2020-07-02: Presented A Lean tactic for normalizing ring expressions with exponents at IJCAR 2020, Paris, France Online.
Paper; Slides; Recording

Teaching

• Lecturer at Logic and Modelling 2023-2024
• Project supervisor at Computer Assisted Proofs 2023-2024
• Lecturer, coordinator at Logic and Modelling 2022-2023
• Project supervisor at Computer Assisted Proofs 2022-2023
• Teaching assistant at Logic and Modelling 2021-2022
• Teaching assistant at Logical Verification 2020-2021
• Teaching assistant at Logical Verification 2019-2020
• Teaching assistant at Grondslagen van de Wiskunde 2018-2019

I am an intuitionist.

on the other hand, computers *really* like types for making code work good.
Juliana, Rat Goddess of Vengeance, @juliana@solarpunk.moe 3rd March 2023.