FP²: Fully in-Place Functional Programming
Anton Lorenzen, Daan Leijen, Wouter Swierstra
I am a PhD student in Computer Science at the University of Edinburgh under the supervision of Sam Lindley. I investigate performance optimizations for functional programming languages, in particular reference counting with in-place reuse.
I have previously been a Software Engineering Intern in the OCaml compiler team at Jane Street where I implemented a modal type system for in-place reuse. During my Masters in Computer Science at the University of Bonn I worked with Daan Leijen on Perceus reference counting in Koka. During my Bachelors in Mathematics at Bonn, I worked with Peter Koepke on the proof assistant Naproche.
Feel free to email me if you want to get in touch.
Publications & Talks
2023
Tail Recursion Modulo Context - An Equational Approach
Daan Leijen, Anton Lorenzen
POPL 2023 [technical report]
2022
Balanced Search Tree Insertion: Recursive is Top-down is Bottom-up
Anton Lorenzen
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
Optimizing Reference Counting with Borrowing
Extended version of my Master thesis [pdf]
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
A Natural Formalization of the Mutilated Checkerboard Problem in Naproche
Adrian De Lon, Peter Koepke, Anton Lorenzen
ITP 2021
2020
Interpreting Mathematical Texts in Naproche-SAD
Adrian De Lon, Peter Koepke, Anton Lorenzen
CICM 2020