• We ran a tutorial on MetaCoq at POPL, on Sunday, January 14th, with Meven Lennon-Bertrand, Matthieu Sozeau, and Théo Winterhalter.
• From September to November I taught the course on proof assistants in the Parisian Master of Research in Computer Science (MPRI) together with Théo Winterhalter.
• Our paper Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions with Dominik Kirst and Niklas Mück was accepted at APLAS ‘23.
• New pre-print on hal: Correct and Complete Type Checking and Certified Erasure for Coq, in Coq, with Matthieu Sozeau, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, and Théo Winterhalter.
• I gave 3 lectures on Coq, MetaCoq, and (verified) extraction at the Proof and Computation 2023 autumn school in Herrsching near Munich in September. Slides for lecture 1 on Coq, lecture 2 on MetaCoq, lecture 3 on verified extraction.
• I will attend ICFP 2023 in Seattle where I served as workshop co-chair with Arthur Azevedo de Amorim.
• I gave a talk on Synthetic Computability in Constructive Type Theory in the special session on proof assistants at CALCO & MFPS 2023 in Bloomington, Indiana.
• I was an invited speaker at TYPES 2023 in Valencia and gave a talk about verified extraction from Coq to OCaml.
• At TYPES, I also gave a talk on Markov’s Principles in Constructive Type Theory, joint work with Dominik Kirst, Bruno da Rocha Paiva, and Vincent Rahli.
• Our paper A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory with Felix Jahn and Gert Smolka was accepted at CPP 2023. Pre-print on hal.
• Our paper Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-one and Truth-table Reducibility in Coq with Felix Jahn was accepted at CSL 2023. Pre-print on hal.
• The TYPES conference in Nantes has lots of interesting talks! I was involved in several:
  • On Tuesday, Tiago Cogumbreiro will present our work Towards a Mechanized Theory of Computation for Education.
  • Immediately afterwards, Felix Jahn will talk about our joint work with Gert Smolka, Myhill Isomorphism Theorem and a Computational Cantor-Bernstein Theorem in Constructive Type Theory.
  • Then I’ll give a talk on Synthetic Turing Reducibility in CIC, joint work with Dominik Kirst.
  • On Wednesday, I’ll be talking about Aspects of a machine-checked intermediate language for extraction from Coq, in MetaCoq, joint work with Matthieu Sozeau.
  • And on Thursday, Dominik Kirst will talk about our Synthetic Versions of the Kleene-Post and Post’s Theorem, joint work with Niklas Mück.
• Our paper Synthetic Kolmogorov Complexity in Coq with Fabian Kunze and Nils Lauermann got accepted at ITP ‘22!
• Two new pre-prints out! With Felix Jahn and Gert Smolka: A Constructive and Synthetic Theory of Reducibility: Myhill’s Isomorphism Theorem and Post’s Problem for Many-one and Truth-table Reducibility in Coq. With Fabian Kunze and Nils Lauermann: Synthetic Kolmogorov Complexity in Coq.
• My paper Parametric Church’s Thesis: Synthetic Computability without Choice got accepted at LFSC ‘22 and won the Rosser Prize. LFCS has free online participation!

Verified extraction and compilation

I am interested in using the Coq proof assistant as a system to obtain verified executable programs: I co-developed verified extraction from Coq to OCaml, I am involved in the MetaCoq project, a formalisation and implementation of Coq in Coq, where I verified type and proof erasure (POPL ‘20), And I am a team member in the CertiCoq project, a verified compiler from Coq to C.

Synthetic computability

Synthetic computability was pioneered by Richman, Bridges, and Bauer in different flavours of constructive logic. In synthetic computability theory, the fact that all definable functions in constructive logic are computable is made explicit via axioms. Thereby, formalisations can focus on the mathematical essence of results and on rigorous simplification of proofs rather than on encoding programs in model of computation.

Since synthetic computability in most presentations assumes the axiom of countable choice the theory becomes anti-classical, i.e. the law of excluded middle is disprovable. When choosing constructive type theory as implemented by the Coq proof assistant as foundation for synthetic computability, classical logic via the law of excluded middle can be consistently assumed.

We gave a general discussion of the axiom CT (Church’s Thesis) in relation to other axioms for Coq’s type theory (CSL ‘21) an introduction to Parametric Church’s Thesis and synthetic computability without choice (LFCS 22), a definition of Kolmogorov complexity (ITP ‘22’), a solution for Post’s problem for many-one and truth-table reducibility (CSL ‘23), and a definition of oracle computability and Turing reductions (APLAS ‘23’).

Synthetic undecidability

Decidability and undecidability proofs are the subarea of computability theory with the most influence on general theoretical computer science. Both kinds of proofs are often intricate and their details are error-prone: Several later retracted results have been published at renowned venues. Synthetic undecidability offers a method to verify the undecidability in a proof assistant such that no doubt remains, without ever dealing with models of computation. This is because all functions definable in Coq’s type theory are by definition computable, and thus undecidability of a problem can be proved by a reduction from Turing machine halting to the problem in question. A prime result is our synthetic undecidability proof of Hilbert’s tenth problem (FSCD ‘19). I co-maintain the Coq Library of Undecidability Proofs, a collaborative project containing machine-checked undecidability proofs.

Formalising models of computation

We have given several machine-checked equivalence proofs between different models of computation such as Turing machines, register machines, the lambda-calculus or partial recursive functions. As part of this work we have proved that the weak call-by-value λ-calculus is reasonable for both time and space (POPL ‘20) and provided a machine-checked version of the result for time (ITP ‘21).

All publications should either be gold open access (i.e. freely accessible via the publisher) or green open access (i.e. uploaded to a pre-print server like arxiv or hal), and links are included below. If a link is missing and you cannot access a publication freely, please drop me an email.

1. Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau, 2023. Verified Extraction from Coq to OCaml,
2. Yannick Forster, Dominik Kirst, and Niklas Mück, 2024. The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions, In: 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024, February 19-23, 2024, Naples, Italy, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 29:1–29:20.
3. Yannick Forster, Dominik Kirst, and Niklas Mück, 2023. Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions, In: Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Taipei, Taiwan, November 26-29, 2023, Proceedings, Lecture Notes in Computer Science, Springer, pp. 155–181.
4. Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, and Théo Winterhalter, 2023. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq,
5. Yannick Forster, Felix Jahn, and Gert Smolka, 2023. A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory, In: CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, Boston, United States.
6. Yannick Forster and Felix Jahn, 2023. Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq, In: 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 13-16, 2023, Warsaw, Poland, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 21:1–21:21.
7. Yannick Forster, Fabian Kunze, and Nils Lauermann, 2022. Synthetic Kolmogorov Complexity in Coq, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, volume 237, pp. 12:1–12:19.
8. Yannick Forster, 2022. Parametric Church’s Thesis: Synthetic Computability Without Choice, In: Logical Foundations of Computer Science, Cham: Springer International Publishing, pp. 70–89.
9. Yannick Forster, Fabian Kunze, Gert Smolka, and Maxi Wuttke, 2021. A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value \(λ\)-Calculus, In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 19:1–19:20.
10. Yannick Forster, Dominik Kirst, and Dominik Wehr, 2021. Completeness theorems for first-order logic analysed in constructive type theory (extended version), J. Log. Comput., volume 31, number 1, pp. 112–151.
11. Yannick Forster, 2021. Church’s Thesis and Related Axioms in Coq’s Type Theory, In: 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 21:1–21:19. (talk)
12. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter, 2020. The MetaCoq Project, J. Autom. Reason., volume 64, number 5, pp. 947–999.
13. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter, 2020. Coq Coq Correct! verification of type checking and erasure for Coq, in Coq, Proc. ACM Program. Lang., volume 4, number POPL, pp. 8:1–8:28.
14. Yannick Forster, Fabian Kunze, and Marc Roth, 2020. The weak call-by-value λ-calculus is reasonable for both time and space, Proc. ACM Program. Lang., volume 4, number POPL, pp. 27:1–27:23.
15. Yannick Forster, Fabian Kunze, and Maxi Wuttke, 2020. Verified programming of Turing machines in Coq, In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, ACM, pp. 114–128.
16. Simon Spies and Yannick Forster, 2020. Undecidability of higher-order unification formalised in Coq, In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, ACM, pp. 143–157.
17. Yannick Forster and Kathrin Stark, 2020. Coq à la carte: a practical approach to modular syntax with binders, In: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, ACM, pp. 186–200.
18. Yannick Forster, Dominik Kirst, and Dominik Wehr, 2020. Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory, In: Logical Foundations of Computer Science - International Symposium, LFCS 2020, Deerfield Beach, FL, USA, January 4-7, 2020, Proceedings, Lecture Notes in Computer Science, Springer, pp. 47–74.
19. Dominique Larchey-Wendling and Yannick Forster, 2020. Hilbert’s Tenth Problem in Coq (extended version), CoRR, volume abs/2003.04604.
20. Yannick Forster and Gert Smolka, 2019. Call-by-Value Lambda Calculus as a Model of Computation in Coq, J. Autom. Reason., volume 63, number 2, pp. 393–413.
21. Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar, 2019. On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control, J. Funct. Program., volume 29, p. e15.
22. Yannick Forster, Dominik Kirst, and Gert Smolka, 2019. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem, In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, ACM, pp. 38–51.
23. Yannick Forster and Dominique Larchey-Wendling, 2019. Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines, In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, ACM, pp. 104–117.
24. Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark, 2019. Call-by-push-value in Coq: operational, equational, and denotational theory, In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, ACM, pp. 118–131.
25. Yannick Forster and Fabian Kunze, 2019. A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus, In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 17:1–17:19.
26. Dominique Larchey-Wendling and Yannick Forster, 2019. Hilbert’s Tenth Problem in Coq, In: 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 27:1–27:20.
27. Fabian Kunze, Gert Smolka, and Yannick Forster, 2018. Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine, In: Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, Lecture Notes in Computer Science, Springer, pp. 264–283.
28. Yannick Forster, Edith Heiter, and Gert Smolka, 2018. Verification of PCP-Related Computational Reductions in Coq, In: Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, Lecture Notes in Computer Science, Springer, pp. 253–269.
29. Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar, 2017. On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control, Proc. ACM Program. Lang., volume 1, number ICFP, pp. 13:1–13:29.
30. Yannick Forster and Gert Smolka, 2017. Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq, In: Interactive Theorem Proving - 8th International Conference, ITP 2017, Brası́lia, Brazil, September 26-29, 2017, Proceedings, Lecture Notes in Computer Science, Springer, pp. 189–206.

Theses

Computability in Constructive Type Theory
PhD thesis, Saarland University, 2021.

On the expressive power of effect handlers and monadic reflection (pdf)
Master’s Thesis, Robinson College, University of Cambridge, 2016.

A Formal and Constructive Theory of Computation (pdf)
Bachelor’s Thesis, Programming Systems Lab, Saarland University, 2014.

Extended Abstracts

• Markov’s Principles in Constructive Type Theory
  Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli
  TYPES ‘23, Valencia, Spain, 2023

• Extraction to OCaml from Coq: Operational Correctness Verified in Coq
  Yannick Forster, Matthieu Sozeau, Pierre Giraud, Pierre-Marie Pédrot, Nicolas Tabareau
  ML Family Workshop, Ljubljana, Slovenia, 2022.

• Towards a Mechanized Theory of Computation for Education
  Tiago Cogumbreiro, Yannick Forster
  TYPES 2022, Nantes, France, 2022.

• Myhill’s Isomorphism Theorem and a Computational Cantor-Bernstein Theorem in Constructive Type Theory
  Yannick Forster, Felix Jahn, Gert Smolka
  TYPES 2022, Nantes, France, 2022.

• Synthetic Turing Reducibility in CIC
  Yannick Forster, Dominik Kirst
  TYPES 2022, Nantes, France, 2022.

• Aspects of a machine-checked intermediate language for extraction from Coq, in MetaCoq
  Yannick Forster, Matthieu Sozeau
  TYPES 2022, Nantes, France, 2022.

• Synthetic Versions of the Kleene-Post and Post’s Theorem
  Dominik Kirst, Niklas Mück, Yannick Forster
  TYPES 2022, Nantes, France, 2022.

• The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoq
  Matthieu Sozeau, Meven Lennon-Bertrand, Yannick Forster
  The first Workshop on the Implementation of Type Systems (WITS). Philadelphia, Pennsylvania, United States / online, 2022.

• Generating induction principles and subterm relations for inductive types using MetaCoq (slides)
  Bohdan Liesnikov, Marcel Ullrich, Yannick Forster
  Coq Workshop 2020, online, 2020.

• Towards Extraction of Continuity Moduli in Coq (pdf) (slides)
  Yannick Forster, Dominik Kirst, Florian Steinberg
  Types 2020, Turin, Italy, 2020.

• A Coq Library of Undecidable Problems (slides) (talk recording)
  Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, Maxi Wuttke
  CoqPL 2020, New Orleans, USA, 2020.

• Coq Coq Codet! - Towards a Verified Toolchain for Coq in MetaCoq (slides)
  Matthieu Sozeau, Yannick Forster, Simon Boulier, Nicolas Tabareau and Théo Winterhalter
  Coq Workshop 2019, Portland, USA, 2019.

• Mechanically verified type and proof erasure for Coq
  Yannick Forster and Matthieu Sozeau
  Facets of Realizability 2019, Paris, France, 2019.

• A constructive Coq library for the mechanization of undecidability (slides)
  Yannick Forster and Dominique Larchey-Wendling
  MLA 2019, Nancy, France, 2019.x

• Towards a library of formalised undecidable problems in Coq: The undecidability of intuitionistic linear logic (slides)
  Yannick Forster and Dominique Larchey-Wendling
  LOLA 2018, Oxford, UK, 2018.

• The strong invariance thesis for a lambda-calculus (slides)
  Yannick Forster, Fabian Kunze, Marc Roth
  LOLA 2017, Reykjavik, Iceland, 2017.

• Verified Extraction from Coq to a Lambda-Calculus (slides)
  Yannick Forster and Fabian Kunze
  Coq Workshop 2016, ITP 2016, Nancy, France, 2016.

Talks since December 2021, for older talks see my old website.

• Synthetic Computability in Constructive Type Theory
  Invited talk in the special session on proof assistants at CALCO & MFPS 2023
  Bloomington, Indiana.

• Verified Extraction from Coq to OCaml
  Invited talk at TYPES 2023.
  Joint work with Matthieu Sozeau, Pierre-Marie Pédrot, and Nicolas Tabareau.

• Synthetic Computability in Constructive Type Theory.
  Talk at the Chocola meeting. June 2nd 2022, Lyon.
  Joint work with joint with Dominik Kirst, Gert Smolka, Felix Jahn, Niklas Mück, Nils Lauermann, Fabian Kunze, and the contributors of the Coq Library of Undecidability Proofs.

• Towards verified extraction from Coq to Ocaml.
  Talk at the Journée scientifique Inria - Nomadic Labs, June 1st 2022, Paris.
  Joint work with Matthieu Sozeau, Pierre Giraud, Pierre-Marie Pédrot, and Nicolas Tabareau.

• Verified Extraction to OCaml from Coq, in Coq.
  Invited Talk at the Conference on Algorithmic Law Design and Implementation. April 28th 2022, Barcelona.
  Joint work with Matthieu Sozeau, Pierre Giraud, Pierre-Marie Pédrot, and Nicolas Tabareau.

Supervised students

Haoyi Zeng, 2023, Bachelor's thesis, co-advised with Dominik Kirst
Post's problem and the priority method in the Calculus of Inductive Constructions

Janis Bailitis, 2024, Bachelor's thesis, co-advised with Dominik Kirst
Löb's theorem in Coq

Fabian Brenner, 2024, Bachelor's thesis, co-advised with Dominik Kirst
The undecidability of finitary PCF in Coq

Niklas Mück, 2021, Bachelor's thesis, co-advised with Dominik Kirst
The Arithmetical Hierarchy and Post’s Theorem in Coq

Roberto Álvarez, 2021, Master's thesis
Mechanized undecidability of subtyping in System F

Felix Jahn, 2020, Bachelor's thesis
Synthetic One-One, Many-One, and Truth-Table Reducibility in Coq

Marcel Ullrich, 2020, Bachelor's thesis
Generating induction principles for nested inductive types in MetaCoq

Dominik Wehr, 2019, Bachelor's thesis, co-advised with Dominik Kirst
A Constructive Analysis of First-Order Completeness Theorems in Coq

Simon Spies, 2019, Bachelor's thesis
Formalising the Undecidability of Higher-Order Unification

Maxi Wuttke, 2018, Bachelor's thesis
Verified Programming Of Turing Machines In Coq

Edith Heiter, 2017, Bachelor's thesis, co-advised with Gert Smolka
Undecidability of the Post Correspondence Problem in Coq

Lectures

• since 2023: Permanent researcher (“chargé de recherche”) in the Cambium team at Inria Paris.
• 2021-2023: Postdoctoral Marie Skłodowska-Curie Fellow in the Gallinette team at Inria Nantes
• 2021: PhD in the group of Gert Smolka at Saarland University
• 2016: MPhil in advanced computer science at the University of Cambridge, with distinction
• 2015: B. Sc. in computer science at Saarland University

Click here for a full but only occasionally updated CV.