Yannick Forster

• From May to August, I had two interns working on the MetaCoq project: Yee-Jian Tan, working on a reimplementation and specification of Coq’s guard condition, and Weituo Dai, working on scope guarantees for meta-programs.
• I am workshop co-chair of ICFP ’24 together with Chandra Nandi.
• I gave an invited talk on Synthetic Computability without Choice at the Panhellenic Logic Symposium in Thessaloniki, reporting on joint work with Dominik Kirst, Gert Smolka, Felix Jahn, Niklas Mück, and Haoyi Zeng.
• Our paper Separating Markov’s Principles, joint work with Liron Cohen, Dominik Kirst, Bruno da Rocha Paiva, and Vincent Rahli, got accepted at LICS ’24.
• Our paper Verified Extraction from Coq to OCaml, joint work with Matthieu Sozeau and Nicolas Tabareau, got accepted at PLDI ’24 and was chosen as a distinguished paper!
• I will attend TYPES ’24. Lots of interesting talks in session 4!
• Our paper The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions with Dominik Kirst and Niklas Mück was accepted at CSL ’24 (pre-print).
• We ran a tutorial on MetaCoq at POPL, on Sunday, January 14th, with Meven Lennon-Bertrand, Matthieu Sozeau, and Théo Winterhalter.
• As of December 1st, I joined the Cambium team at Inria Paris on a permanent position.
• 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 (PLDI ’24); 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), a definition of oracle computability and Turing reductions (APLAS ‘23’), and a proof of Post’s hierarchy theorem (CSL ‘24’).

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).

1. Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, and Théo Winterhalter. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq

1. Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, and Vincent Rahli. Separating Markov's Principles, LICS 2024.
2. Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau. Verified Extraction from Coq to OCaml, PLDI 2024.
3. Yannick Forster, Dominik Kirst, and Niklas Mück. The Kleene-Post and Post’s Theorem in the Calculus of Inductive Constructions, CSL 2024.
4. Yannick Forster, Dominik Kirst, and Niklas Mück. Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions, APLAS 2023.
5. Yannick Forster, Felix Jahn, and Gert Smolka. A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory, CPP 2023.
6. Yannick Forster and Felix Jahn. Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-One and Truth-Table Reducibility in Coq, CSL 2023.
7. Yannick Forster, Fabian Kunze, and Nils Lauermann. Synthetic Kolmogorov Complexity in Coq, ITP 2022.
8. Yannick Forster, 2022. Parametric Church’s Thesis: Synthetic Computability Without Choice, LFCS 2022.
9. Yannick Forster, Fabian Kunze, Gert Smolka, and Maxi Wuttke. A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus, ITP 2021.
10. Yannick Forster. Church’s Thesis and Related Axioms in Coq’s Type Theory, CSL 2021. (talk)
11. Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Théo Winterhalter. Coq Coq Correct! verification of type checking and erasure for Coq, in Coq, POPL 2020.
12. Yannick Forster, Fabian Kunze, and Marc Roth. The weak call-by-value λ-calculus is reasonable for both time and space, POPL 2020.
13. Yannick Forster, Fabian Kunze, and Maxi Wuttke. Verified programming of Turing machines in Coq, CPP 2020.
14. Simon Spies and Yannick Forster. Undecidability of higher-order unification formalised in Coq, CPP 2020.
15. Yannick Forster and Kathrin Stark. Coq à la carte: a practical approach to modular syntax with binders, CPP 2020.
16. Yannick Forster, Dominik Kirst, and Dominik Wehr. Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory, LFCS 2020.
17. Yannick Forster and Fabian Kunze. A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus, ITP 2019.
18. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq, FSCD 2019.
19. Yannick Forster, Dominik Kirst, and Gert Smolka. On synthetic undecidability in Coq, with an application to the Entscheidungsproblem, CPP 2019.
20. Yannick Forster and Dominique Larchey-Wendling. Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines, CPP 2019.
21. Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark. Call-by-push-value in Coq: operational, equational, and denotational theory, CPP 2019.
22. Fabian Kunze, Gert Smolka, and Yannick Forster. Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine, APLAS 2018.
23. Yannick Forster, Edith Heiter, and Gert Smolka. Verification of PCP-Related Computational Reductions in Coq, ITP 2018.
24. Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control, ICFP 2017.
25. Yannick Forster and Gert Smolka. Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq, ITP 2017.

1. Yannick Forster, Dominik Kirst, and Dominik Wehr. Completeness theorems for first-order logic analysed in constructive type theory (extended version), J. Log. Comput. , volume 31, number 1, pp. 112–151.
2. Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. The MetaCoq Project, J. Autom. Reason., volume 64, number 5, pp. 947–999.
3. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq (extended version), LMCS, Volume 18, Issue 1.
4. Yannick Forster and Gert Smolka. Call-by-Value Lambda Calculus as a Model of Computation in Coq, J. Autom. Reason., volume 63, number 2, pp. 393–413.
5. Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar. On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control, J. Funct. Program., volume 29, p. e15.

• Post’s Problem in Constructive Mathematics
  Haoyi Zeng, Yannick Forster, Dominik Kirst, Takako Nemoto
  CCC ’24, Nice, France, 2024

• A zoo of continuity properties in constructive type theory
  Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot, Matthieu Piquerez
  CCC ’24, Nice, France, 2024

• A zoo of continuity properties in constructive type theory
  Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot, Matthieu Piquerez
  TYPES ’24, Copenhagen, Denmark, 2024

• Limited Principles of Omniscience in Constructive Type Theory
  Bruno da Rocha Paiva, Liron Cohen, Yannick Forster, Dominik Kirst, Vincent Rahli
  TYPES ’24, Copenhagen, Denmark, 2024

• Post’s Problem and the Priority Method in CIC
  Haoyi Zeng, Yannick Forster, Dominik Kirst
  TYPES ’24, Copenhagen, Denmark, 2024

• 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.

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.

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

• Synthetic Computability without Choice
  Invited talk at the 14th Panhellenic Logic Symposium.
  

• A zoo of continuity properties in constructive type theory
  Talks at TYPES 2024.
  Joint work with Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot, Matthieu Piquerez.

• 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

• Mathis Bouverot-Dupuis, 2024, 4th year ENS intern
  Meta-programming for and with dependent types.

• Thomas Lamiaux, 2024, PhD student, co-supervised with Nicolas Tabareau and Matthieu Sozeau
  Verifying Coq’s guard condition.

• Yee Jian Tan, 2024, MPRI M1 internship
  A specification of Coq’s guard condition in MetaCoq.

• Weituo Dai, 2024, MPRI M2 internship
  Meta-programming with guarantees in MetaCoq.

• 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

• Winter 2024: Proof assistants, M2 course, Parisian Master in Research in Computer Science (MPRI), with Théo Winterhalter.
• Winter 2023: Proof assistants, M2 course, Parisian Master in Research in Computer Science (MPRI), with Théo Winterhalter.
• Winter 2022/2023: Proof assistants, M2 course, Parisian Master in Research in Computer Science (MPRI), with Matthieu Sozeau and Théo Winterhalter.
• Winter 2020/2021: Advanced Coq Programming, Block course, Programming Systems Lab.
• Winter 2018/2019: Programming 1, Basic course, Programming Systems Lab.
• Summer 2018: Advanced Coq Programming, Block course, Programming Systems Lab.
• Winter 2017: Category Theory, Seminar, Programming Systems Lab.
• Summer 2017: Mathematics Precourse, Saarland University.
• Summer 2017: Didactic Seminar for Student TAs in Programming 1, Reactive Systems Group.

• 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.