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 | TAProgramming 1Basic 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 TAIntroduction to System Architecture Basic course, Real-Time and Embedded Systems Lab. |

Summer 2015 | Coach and Organiser Mathematics Precourse Saarland University. |

Summer 2015 | Student TAIntroduction to Computational LogicCore course, Programming Systems Lab. |

Winter 2015/16 | Student TAIntroduction to Theoretical Computer ScienceBasic course, Computational Complexity. |

Summer 2014 | Student TALinear Algebra 2Basic course, Tropical Geometry Group. |

Winter 2013/14 | Student TALinear Algebra 1Basic course, Tropical Geometry Group. |

Winter 2013/14 | Student TAProgramming 1Basic course, Dependent Systems Group. |

Summer 2013 | Student TAMathematics Precourse Saarland University. |

Mail: | fkunze-ps at fkunze.de |