I am a PhD student at the University of Edinburgh supervised by
Sam Lindley and
Daan Leijen.
I have been an intern in the RiSE
group at Microsoft Research and the OCaml compiler team at Jane Street.
Before that, I studied mathematics and computer science at the University of Bonn, Germany.
I am interested in improving functional algorithms with techniques such as defunctionalization, in-place reuse and tail recursion modulo cons.
I am also working on optimizations for Perceus-style reference counting (as implemented in Koka)
and modal type systems for in-place reuse.
Previously, I worked on the Naproche proof assistant
which provides an elegant natural language interface for mathematical proofs.
Feel free to email me if you want to get in touch.
Publications
2023
A Functional Correspondence between Top-down and Bottom-up Tree Algorithms
Anton Lorenzen, Daan Leijen, Wouter Swierstra, Sam Lindley
FP²: Fully in-Place Functional Programming
Anton Lorenzen, Daan Leijen, Wouter Swierstra
Tail Recursion Modulo Context - An Equational Approach
Daan Leijen, Anton Lorenzen
2022
Reference Counting with Frame Limited Reuse
Anton Lorenzen, Daan Leijen
Web-Naproche
Anton Lorenzen, Peter Koepke
CICM 2022 (part of the CICM’22 System Entries, with Boris Shminke)
2021
Beautiful Formalizations in Isabelle/Naproche
Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Erik Sturzenhecker
CICM 2021
The Isabelle/Naproche Natural Language Proof Assistant
Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Makarius Wenzel
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche
Adrian De Lon, Peter Koepke, Anton Lorenzen
2020
Interpreting Mathematical Texts in Naproche-SAD
Adrian De Lon, Peter Koepke, Anton Lorenzen
CICM 2020
Talks
2023
A Functional Correspondence between Top-down and Bottom-up Tree Algorithms
Anton Lorenzen
Microsoft Research
2022
Balanced Search Tree Insertion: Recursive is Top-down is Bottom-up
Anton Lorenzen
Stackless Traversals with Zippers
Anton Lorenzen
Universiteit Utrecht
[slides]
2021 & 2020
Dealing with Soft Types in Naproche’s Logical Backend
Adrian De Lon, Peter Koepke, Anton Lorenzen
AITP 2021
ForTheL for Type Theory
Adrian De Lon, Peter Koepke, Anton Lorenzen
AITP 2020
Notes
2021
Optimizing Reference Counting with Borrowing
Extended version of my Master thesis
[pdf]
Built with Pure v2. Impressum