Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. - Yannick Forster 002; Gert Smolka (ITP, 2017)

On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. - Yannick Forster 002; Ohad Kammar; Sam Lindley; Matija Pretnar (Proc. ACM Program. Lang., 2017)

Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. - Fabian Kunze; Gert Smolka; Yannick Forster 002 (APLAS, 2018)

Verification of PCP-Related Computational Reductions in Coq. - Yannick Forster 002; Edith Heiter; Gert Smolka (ITP, 2018)

On synthetic undecidability in coq, with an application to the entscheidungsproblem. - Yannick Forster 002; Dominik Kirst; Gert Smolka (CPP, 2019)

Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. - Yannick Forster 002; Dominique Larchey-Wendling (CPP, 2019)

Call-by-push-value in coq: operational, equational, and denotational theory. - Yannick Forster 002; Steven Schäfer; Simon Spies; Kathrin Stark (CPP, 2019)

A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. - Yannick Forster 002; Fabian Kunze (ITP, 2019)

Hilbert's Tenth Problem in Coq. - Dominique Larchey-Wendling; Yannick Forster 002 (FSCD, 2019)

A certifying extraction with time bounds from Coq to call-by-value $λ$-calculus. - Yannick Forster 002; Fabian Kunze (CoRR, 2019)

Call-by-Value Lambda Calculus as a Model of Computation in Coq. - Yannick Forster 002; Gert Smolka (J. Autom. Reason., 2019)

Verified programming of Turing machines in Coq. - Yannick Forster 002; Fabian Kunze; Maxi Wuttke (CPP, 2020)

Coq à la carte: a practical approach to modular syntax with binders. - Yannick Forster 002; Kathrin Stark (CPP, 2020)

Undecidability of higher-order unification formalised in Coq. - Simon Spies; Yannick Forster 002 (CPP, 2020)

Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version). - Yannick Forster 002; Dominik Kirst; Dominik Wehr (CoRR, 2020)

Generating induction principles and subterm relations for inductive types using MetaCoq. - Bohdan Liesnikov; Marcel Ullrich; Yannick Forster 002 (CoRR, 2020)

The MetaCoq Project. - Matthieu Sozeau; Abhishek Anand; Simon Boulier; Cyril Cohen; Yannick Forster 002; Fabian Kunze; Gregory Malecha; Nicolas Tabareau; Théo Winterhalter (J. Autom. Reason., 2020)

The weak call-by-value λ-calculus is reasonable for both time and space. - Yannick Forster 002; Fabian Kunze; Marc Roth (Proc. ACM Program. Lang., 2020)

Coq Coq correct! verification of type checking and erasure for Coq, in Coq. - Matthieu Sozeau; Simon Boulier; Yannick Forster 002; Nicolas Tabareau; Théo Winterhalter (Proc. ACM Program. Lang., 2020)

Church's Thesis and Related Axioms in Coq's Type Theory. - Yannick Forster 002 (CSL, 2021)

A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. - Yannick Forster 002; Fabian Kunze; Gert Smolka; Maxi Wuttke (ITP, 2021)

Completeness theorems for first-order logic analysed in constructive type theory. - Yannick Forster 002; Dominik Kirst; Dominik Wehr (J. Log. Comput., 2021)

Computability in constructive type theory. - Yannick Forster 002 (2021)

Synthetic Kolmogorov Complexity in Coq. - Yannick Forster 002; Fabian Kunze; Nils Lauermann (ITP, 2022)

Parametric Church's Thesis: Synthetic Computability Without Choice. - Yannick Forster 002 (LFCS, 2022)

Hilbert's Tenth Problem in Coq (Extended Version). - Dominique Larchey-Wendling; Yannick Forster 002 (Log. Methods Comput. Sci., 2022)

Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions. - Yannick Forster 002; Dominik Kirst; Niklas Mück (APLAS, 2023)

A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). - Yannick Forster 002; Felix Jahn; Gert Smolka (CPP, 2023)

Constructive and Synthetic Reducibility Degrees: Post's Problem for Many-One and Truth-Table Reducibility in Coq. - Yannick Forster 002; Felix Jahn (CSL, 2023)

The Kleene-Post and Post's Theorem in the Calculus of Inductive Constructions. - Yannick Forster 002; Dominik Kirst; Niklas Mück (CSL, 2024)

Separating Markov's Principles. - Liron Cohen 001; Yannick Forster 002; Dominik Kirst; Bruno da Rocha Paiva; Vincent Rahli (LICS, 2024)

Verified Extraction from Coq to OCaml. - Yannick Forster 002; Matthieu Sozeau; Nicolas Tabareau (Proc. ACM Program. Lang., 2024)

Synthetic Mathematics for the Mechanisation of Computability Theory and Logic (Invited Talk). - Yannick Forster 002 (CSL, 2025)

A Zoo of Continuity Properties in Constructive Type Theory. - Martin Baillon; Yannick Forster 002; Assia Mahboubi; Pierre-Marie Pédrot; Matthieu Piquerez (FSCD, 2025)

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. - Matthieu Sozeau; Yannick Forster 002; Meven Lennon-Bertrand; Jakob Botsch Nielsen; Nicolas Tabareau; Théo Winterhalter (J. ACM, 2025)