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
Draft [technical report] [AddressC]

FP²: Fully in-Place Functional Programming

Anton Lorenzen, Daan Leijen, Wouter Swierstra
ICFP 2023 [technical report] [hackernews]

Tail Recursion Modulo Context - An Equational Approach

Daan Leijen, Anton Lorenzen
POPL 2023 [technical report]

2022

Reference Counting with Frame Limited Reuse

Anton Lorenzen, Daan Leijen
ICFP 2022 [technical report]

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
CADE 2021 [springer]

A Natural Formalization of the Mutilated Checkerboard Problem in Naproche

Adrian De Lon, Peter Koepke, Anton Lorenzen
ITP 2021 [pdf]

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
SPLS [slides]

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]

Favorite Papers