Tail Recursion Modulo Context: An Equational Approach (extended version)
Daan Leijen, Anton Lorenzen
Draft
[pdf]
I am pursuing a PhD in programming languages at the University of Edinburgh, where I am supervised by Sam Lindley and Daan Leijen. I have interned at the RiSE group of Microsoft Research and the OCaml compiler team of Jane Street, where I worked on Koka and (modal) uniqueness types. I hold a BSc Mathematics and an MSc Computer Science from the University of Bonn, Germany.
Email: <firstname> . <lastname> @ed.ac.uk
Publications
Performance Optimizations for Functional Programming Languages
Modal Effect Types
Wenhao Tang, Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley, Anton Lorenzen
OOPSLA 2025
[technical report]
Oxidizing OCaml with Modal Memory Management
Anton Lorenzen, Leo White, Stephen Dolan, Richard A. Eisenberg, Sam Lindley
The Functional Essence of Imperative Binary Search Trees
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
Reference Counting with Frame Limited Reuse
Anton Lorenzen, Daan Leijen
Optimizing Reference Counting with Borrowing
Master Thesis
supervised by Daan Leijen and Heiko Röglin [extended pdf]
Natural Language Proof Assistants
Web-Naproche
Anton Lorenzen, Peter Koepke
CICM 2022
[doi]
Beautiful Formalizations in Isabelle/Naproche
Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Erik Sturzenhecker
CICM 2021
[doi]
The Isabelle/Naproche Natural Language Proof Assistant
Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz, Makarius Wenzel
CADE 2021
[doi]
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche
Adrian De Lon, Peter Koepke, Anton Lorenzen
ITP 2021
[pdf]
Dealing with Soft Types in Naproche’s Logical Backend
Adrian De Lon, Peter Koepke, Anton Lorenzen
AITP 2021
Interpreting Mathematical Texts in Naproche-SAD
Adrian De Lon, Peter Koepke, Anton Lorenzen
CICM 2020
[doi]
ForTheL for Type Theory
Adrian De Lon, Peter Koepke, Anton Lorenzen
AITP 2020