Reference Counting with Frame Limited Reuse
Anton Lorenzen, Daan Leijen
submitted to PLDI 2022 [technical report]
I am a Master student of Computer Science at the University of Bonn currently looking for PhD positions. I have previously worked with Andrey Mokhov on Algebraic graphs, with Peter Koepke on the proof assistant Naproche and with Daan Leijen on Koka.
Publications
2022
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
Software
Edmonds algorithm in Koka and C++
A solver for the (non-bipartite) maximum cardinality matching problem
Lean Formalization of the Calculus of Constructions
including a partially verified type checker
Agda Formalization of Algebraic Graphs
together with Andrey Mokhov, Alexandre Moine and @Rotsor.