Fabian Kunze

Publication Activity (10 Years)

Years Active: 2016-2022
Publications (10 Years): 12

Top Topics

Automatically Discovering

Comprehensive Set

Kolmogorov Complexity

Top Venues

Proc. ACM Program. Lang.

Publications

Yannick Forster, Fabian Kunze, Nils Lauermann
Synthetic Kolmogorov Complexity in Coq. ITP (2022)
Yannick Forster, Fabian Kunze, Gert Smolka, Maximilian Wuttke
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. ITP (2021)
Lennard Gäher, Fabian Kunze
Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. ITP (2021)
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
The MetaCoq Project. J. Autom. Reason. 64 (5) (2020)
Yannick Forster, Fabian Kunze, Marc Roth
The weak call-by-value λ-calculus is reasonable for both time and space. Proc. ACM Program. Lang. 4 (POPL) (2020)
Yannick Forster, Fabian Kunze, Maximilian Wuttke
Verified programming of Turing machines in Coq. CPP (2020)
Yannick Forster, Fabian Kunze, Marc Roth
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space. CoRR (2019)
Yannick Forster, Fabian Kunze
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. ITP (2019)
Yannick Forster, Fabian Kunze
A certifying extraction with time bounds from Coq to call-by-value $λ$-calculus. CoRR (2019)
Fabian Kunze, Gert Smolka, Yannick Forster
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine. CoRR (2018)
Fabian Kunze, Gert Smolka, Yannick Forster
Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. APLAS (2018)
Fabian Kunze
Towards the Integration of an Intuitionistic First-Order Prover into Coq. HaTT@IJCAR (2016)