Fabian Kunze

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