Draft
Anton Lorenzen
PhD researcher · programming languages · University of Edinburgh
I am pursuing a PhD in programming languages at the University of Edinburgh, supervised by Sam Lindley and Daan Leijen. I have interned at the RiSE group at Microsoft Research and the OCaml compiler team at Jane Street, where I worked on Koka and (modal) uniqueness types. I hold a BSc in Mathematics and an MSc in Computer Science from the University of Bonn, Germany.
anton.lorenzen@ed.ac.uk
Publications
ICALP 2026
Persistent Amortised Analysis, Operationally
Haskell 2025
Lightweight Testing of Persistent Amortized Time Complexity in the Credit Monad
ICFP 2025 Distinguished Paper
First-Order Laziness
JFP Special Issue
Tail Recursion Modulo Context: An Equational Approach (extended version)
OOPSLA 2025
Modal Effect Types
ICFP 2024
Oxidizing OCaml with Modal Memory Management
PLDI 2024
The Functional Essence of Imperative Binary Search Trees
ICFP 2023
FP²: Fully in-Place Functional Programming
POPL 2023
Tail Recursion Modulo Context: An Equational Approach
ICFP 2022
Reference Counting with Frame Limited Reuse
Master Thesis · University of Bonn
Optimizing Reference Counting with Borrowing
CICM 2022
Web-Naproche
CICM 2021
Beautiful Formalizations in Isabelle/Naproche
CADE 2021
The Isabelle/Naproche Natural Language Proof Assistant
ITP 2021
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche
AITP 2021
Dealing with Soft Types in Naproche's Logical Backend
CICM 2020
Interpreting Mathematical Texts in Naproche-SAD
AITP 2020