Oxidizing OCaml with Modal Memory Management
Anton Lorenzen, Leo White, Stephen Dolan, Richard A. Eisenberg, Sam Lindley
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
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
Master Thesis
Optimizing Reference Counting with Borrowing
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