| 2026 | ESOP | Code Generation via Meta-programming in Dependently Typed Proof Assistants. | Mathis Bouverot-Dupuis, Yannick Forster |
| 2026 | FSCD | Not Choosing Is Still a Choice: Constructive mathematics without any choice. | Martin Baillon, Yannick Forster, Dominik Kirst, Assia Mahboubi, Pierre-Marie Pdrot |
| 2026 | STOC | Determination of the Fifth Busy Beaver Value. | Justin Blanchard, Daniel Briggs, Konrad Deka, Nathan Fenner, Yannick Forster, Georgi Georgiev (Skelet), Matthew L. House, Maja Kadziolka, Pavel Kropitz, Shawn Ligocki, mxdys, Mateusz Nasciszewski, Tristan Strin, Chris Xu, Jason Yuen, Tho Zimmermann |
| 2025 | CSL | Synthetic Mathematics for the Mechanisation of Computability Theory and Logic (Invited Talk). | Yannick Forster |
| 2025 | FSCD | A Zoo of Continuity Properties in Constructive Type Theory. | Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pdrot, Matthieu Piquerez |
| 2024 | CSL | The Kleene-Post and Post's Theorem in the Calculus of Inductive Constructions. | Yannick Forster, Dominik Kirst, Niklas Mck |
| 2024 | LICS | Separating Markov's Principles. | Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli |
| 2023 | APLAS | Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions. | Yannick Forster, Dominik Kirst, Niklas Mck |
| 2023 | CPP | A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). | Yannick Forster, Felix Jahn, Gert Smolka |
| 2023 | CSL | Constructive and Synthetic Reducibility Degrees: Post's Problem for Many-One and Truth-Table Reducibility in Coq. | Yannick Forster, Felix Jahn |
| 2022 | ITP | Synthetic Kolmogorov Complexity in Coq. | Yannick Forster, Fabian Kunze, Nils Lauermann |
| 2022 | LFCS | Parametric Church's Thesis: Synthetic Computability Without Choice. | Yannick Forster |
| 2021 | CSL | Church's Thesis and Related Axioms in Coq's Type Theory. | Yannick Forster |
| 2021 | ITP | A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. | Yannick Forster, Fabian Kunze, Gert Smolka, Maxi Wuttke |
| 2020 | CPP | Verified programming of Turing machines in Coq. | Yannick Forster, Fabian Kunze, Maxi Wuttke |
| 2020 | CPP | Coq la carte: a practical approach to modular syntax with binders. | Yannick Forster, Kathrin Stark |
| 2020 | CPP | Undecidability of higher-order unification formalised in Coq. | Simon Spies, Yannick Forster |
| 2020 | HCI | Measuring Driver Distraction with the Box Task - A Summary of Two Experimental Studies. | Tina Morgenstern, Daniel Trommler, Yannick Forster, Frederik Naujoks, Sebastian Hergeth, Josef F. Krems, Andreas Keinath |
| 2020 | LFCS | Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory. | Yannick Forster, Dominik Kirst, Dominik Wehr |
| 2019 | CPP | On synthetic undecidability in coq, with an application to the entscheidungsproblem. | Yannick Forster, Dominik Kirst, Gert Smolka |
| 2019 | CPP | Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. | Yannick Forster, Dominique Larchey-Wendling |
| 2019 | CPP | Call-by-push-value in coq: operational, equational, and denotational theory. | Yannick Forster, Steven Schfer, Simon Spies, Kathrin Stark |
| 2019 | ITP | A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. | Yannick Forster, Fabian Kunze |
| 2018 | APLAS | Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. | Fabian Kunze, Gert Smolka, Yannick Forster |
| 2018 | ITP | Verification of PCP-Related Computational Reductions in Coq. | Yannick Forster, Edith Heiter, Gert Smolka |
| 2017 | ITP | Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. | Yannick Forster, Gert Smolka |