I worked at the programming systems lab until 2022 on the mechanisation of complexity theory. For that, I investigated the use of a lambda calculus as a model of computation with resource bounds, connecting its resource consumption with models used in complexity theory. Furthermore, I worked on automating correctness and resource consumption proofs for programms of the lambda calculus in the Coq proof assistant.
I did my Bachelor's thesis and a Research Immersion Lab on verified complexity theory at this chair.
Synthetic Kolmogorov Complexity in Coq (preprint) (doi)
Yannick Forster, Fabian Kunze and Nils Lauermann
ITP 2022.
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq (pdf) (doi)
Lennard Gäher, Fabian Kunze
ITP 2021.
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value λ-Calculus (pdf) (doi)
Yannick Forster, Fabian Kunze, Gert Smolka, Maximilan Wuttke
ITP 2021.
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space (pdf)
Yannick Forster, Fabian Kunze, Marc Roth
POPL 2020, New Orleans, USA, 2020.
Verified Programming of Turing Machines in Coq (pdf)(slides)
Yannick Forster, Fabian Kunze, Maximilian Wuttke
CPP 2020, New Orleans, USA, 2020.
The MetaCoq Project (pdf) (doi)
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
Journal of Automated Reasoning, 2020.
A certifying extraction with time bounds from Coq to call-by-value λ-calculus (pdf)(slides)
Yannick Forster and Fabian Kunze
ITP 2019, Portland, USA, 2019. Pre-print on arxiv.
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine (pdf)
Fabian Kunze, Gert Smolka, Yannick Forster
APLAS 2018, Wellington, New Zealand, 2018
A Coq Library of Undecidable Problems (pdf)
Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, Maximilian Wuttke
CoqPL 2020, New Orleans, USA, 2020.
The strong invariance thesis for a lambda-calculus
Yannick Forster, Fabian Kunze, Marc Roth
LOLA 2017, Reykjavik, Iceland, 2017.
Verified Extraction from Coq to a Lambda-Calculus (pdf) (slides)
Yannick Forster and Fabian Kunze
Coq Workshop 2016, ITP 2016, Nancy, 2016.
Verified Compilation of Weak Call-by-Value Lambda-Calculus into Combinators and Closures (pdf)
Fabian Kunze
Bachelor's Thesis, Programming Systems Lab, Saarland University, 2015.
Nils Lauermann, 2021, Bachelor's thesis
A Formalization of Kolmogorov Complexity in Synthetic Computability Theory
Lennard Gäher, 2020, Bachelor's thesis
Towards a Formal Proof of the Cook-Levin Theorem
| Winter 2021/22 | TA Programming 1 Basic course, Programming Systems Lab. |
| Winter 2020/21 | Organiser and Lecturer Advanced Coq Programming Block course, Programming Systems Lab. |
| Summer 2020 | Organiser and Advisor Functional Programming Proseminar, Programming Systems Lab. |
| Winter 2019/20 | TA Semantics Core Lecture, Programming Systems Lab. |
| Summer 2019 | Organiser and Advisor Functional Programming Proseminar, Programming Systems Lab. |
| Summer 2018 | Organiser and Advisor Functional Programming Proseminar, Programming Systems Lab. |
| Summer 2018 | Advisor and Lecturer Advanced Coq Programming Block course, Programming Systems Lab. |
| Winter 2016/17 | Advisor Category Theory Seminar, Programming Systems Lab. |
| Winter 2016/17 | Student TA Automated Reasoning 1 Core course, Automation of Logic. |
| Summer 2016 | Coach and Organiser Mathematics Precourse Saarland University. |
| Summer 2016 | Student TA Introduction to System Architecture Basic course, Real-Time and Embedded Systems Lab. |
| Summer 2015 | Coach and Organiser Mathematics Precourse Saarland University. |
| Summer 2015 | Student TA Introduction to Computational Logic Core course, Programming Systems Lab. |
| Winter 2015/16 | Student TA Introduction to Theoretical Computer Science Basic course, Computational Complexity. |
| Summer 2014 | Student TA Linear Algebra 2 Basic course, Tropical Geometry Group. |
| Winter 2013/14 | Student TA Linear Algebra 1 Basic course, Tropical Geometry Group. |
| Winter 2013/14 | Student TA Programming 1 Basic course, Dependent Systems Group. |
| Summer 2013 | Student TA Mathematics Precourse Saarland University. |
| Mail: | fkunze-ps at fkunze.de |