Yannick Forster

48 papers A* 1B 21Misc 2Journal 22Unranked 1

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Code Generation via Meta-programming in Dependently Typed Proof Assistants. ESOP (1) Mathis Bouverot-Dupuis, Yannick Forster
2025	B	`ed.`	16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025 ITP Yannick Forster, Chantal Keller
2025	B	`conf`	A Zoo of Continuity Properties in Constructive Type Theory. FSCD Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot, Matthieu Piquerez
2025	J	`jnl`	Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. J. ACM Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter
2025	J	`jnl`	Determination of the fifth Busy Beaver value. CoRR The bbchallenge Collaboration, Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev, Matthew L. House, Rachel Hunter, Iijil, Maja Kadziolka, Pavel Kropitz, Shawn Ligocki, mxdys, Mateusz Nasciszewski, savask, Tristan Stérin, Chris Xu, Jason Yuen, Théo Zimmermann
2025	B	`conf`	Synthetic Mathematics for the Mechanisation of Computability Theory and Logic (Invited Talk). CSL Yannick Forster
2024	A*	`conf`	Separating Markov's Principles. LICS Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli
2024	B	`conf`	The Kleene-Post and Post's Theorem in the Calculus of Inductive Constructions. CSL Yannick Forster, Dominik Kirst, Niklas Mück
2024	J	`jnl`	Verified Extraction from Coq to OCaml. Proc. ACM Program. Lang. Yannick Forster, Matthieu Sozeau, Nicolas Tabareau
2023	B	`conf`	A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). CPP Yannick Forster, Felix Jahn, Gert Smolka
2023	B	`conf`	Constructive and Synthetic Reducibility Degrees: Post's Problem for Many-One and Truth-Table Reducibility in Coq. CSL Yannick Forster, Felix Jahn
2023	B	`conf`	Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions. APLAS Yannick Forster, Dominik Kirst, Niklas Mück
2023	J	`jnl`	Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions. CoRR Yannick Forster, Dominik Kirst, Niklas Mück
2022	J	`jnl`	Hilbert's Tenth Problem in Coq (Extended Version). Log. Methods Comput. Sci. Dominique Larchey-Wendling, Yannick Forster
2022	Misc	`conf`	Parametric Church's Thesis: Synthetic Computability Without Choice. LFCS Yannick Forster
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`	Church's Thesis and Related Axioms in Coq's Type Theory. CSL Yannick Forster
2021	J	`jnl`	Completeness theorems for first-order logic analysed in constructive type theory. J. Log. Comput. Yannick Forster, Dominik Kirst, Dominik Wehr
2021	—	`—`	Computability in constructive type theory. Yannick Forster
2021	J	`jnl`	Parametric Church's Thesis: Synthetic Computability without Choice. CoRR Yannick Forster
2020	J	`jnl`	Church's thesis and related axioms in Coq's type theory. CoRR Yannick Forster
2020	J	`jnl`	Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version). CoRR Yannick Forster, Dominik Kirst, Dominik Wehr
2020	Misc	`conf`	Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory. LFCS Yannick Forster, Dominik Kirst, Dominik Wehr
2020	J	`jnl`	Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proc. ACM Program. Lang. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter
2020	B	`conf`	Coq à la carte: a practical approach to modular syntax with binders. CPP Yannick Forster, Kathrin Stark
2020	J	`jnl`	Generating induction principles and subterm relations for inductive types using MetaCoq. CoRR Bohdan Liesnikov, Marcel Ullrich, Yannick Forster
2020	J	`jnl`	Hilbert's Tenth Problem in Coq. CoRR Dominique Larchey-Wendling, Yannick Forster
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`	Undecidability of higher-order unification formalised in Coq. CPP Simon Spies, Yannick Forster
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`	Call-by-Value Lambda Calculus as a Model of Computation in Coq. J. Autom. Reason. Yannick Forster, Gert Smolka
2019	B	`conf`	Call-by-push-value in coq: operational, equational, and denotational theory. CPP Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark
2019	B	`conf`	Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. CPP Yannick Forster, Dominique Larchey-Wendling
2019	B	`conf`	Hilbert's Tenth Problem in Coq. FSCD Dominique Larchey-Wendling, Yannick Forster
2019	B	`conf`	On synthetic undecidability in coq, with an application to the entscheidungsproblem. CPP Yannick Forster, Dominik Kirst, Gert Smolka
2019	J	`jnl`	On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control. J. Funct. Program. Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar
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
2018	B	`conf`	Verification of PCP-Related Computational Reductions in Coq. ITP Yannick Forster, Edith Heiter, Gert Smolka
2017	J	`jnl`	On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. Proc. ACM Program. Lang. Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar
2017	J	`jnl`	Verification of PCP-Related Computational Reductions in Coq. CoRR Yannick Forster, Edith Heiter, Gert Smolka
2017	B	`conf`	Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. ITP Yannick Forster, Gert Smolka
2016	J	`jnl`	On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control. CoRR Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar