I am a researcher (“chargé de recherche”) at Inria in the Cambium team in Paris.
My research focuses on different aspects of computation in relation to (constructive) type theory, often involving the proof assistant Coq. See below for a list of projects. I am excited about any potential collaborator for any of these topics, if you are interested in working with me please get in touch no matter your location, level of expertise, or academic experience – including no or little expertise or experience!
Before joining Cambium, I was a Marie SkłodowskaCurie fellow at Inria in the Gallinette team in Nantes. And before that, I did my PhD at Saarland University with Gert Smolka.
News
 Our paper The KleenePost and Post’s Theorem in the Calculus of Inductive Constructions with Dominik Kirst and Niklas Mück was accepted at CSL ‘24 (preprint).
 I am workshop cochair of ICFP ‘24 together with Chandra Nandi.
 As of December 1st, I joined the Cambium team at Inria Paris on a permanent position.
older news
 We ran a tutorial on MetaCoq at POPL, on Sunday, January 14th, with Meven LennonBertrand, 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 preprint on hal: Correct and Complete Type Checking and Certified Erasure for Coq, in Coq, with Matthieu Sozeau, Meven LennonBertrand, 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 cochair 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 CantorBernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory with Felix Jahn and Gert Smolka was accepted at CPP 2023. Preprint on hal.
 Our paper Constructive and Synthetic Reducibility Degrees: Post’s Problem for Manyone and Truthtable Reducibility in Coq with Felix Jahn was accepted at CSL 2023. Preprint 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 CantorBernstein 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 machinechecked 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 KleenePost 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 preprints out! With Felix Jahn and Gert Smolka: A Constructive and Synthetic Theory of Reducibility: Myhill’s Isomorphism Theorem and Post’s Problem for Manyone and Truthtable 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!
Projects
Verified extraction and compilation
I am interested in using the Coq proof assistant as a system to obtain verified executable programs: I codeveloped 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 anticlassical, 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 manyone and truthtable 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 errorprone: 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 comaintain the Coq Library of Undecidability Proofs, a collaborative project containing machinechecked undecidability proofs.
Formalising models of computation
We have given several machinechecked equivalence proofs between different models of computation such as Turing machines, register machines, the lambdacalculus or partial recursive functions. As part of this work we have proved that the weak callbyvalue λcalculus is reasonable for both time and space (POPL ‘20) and provided a machinechecked version of the result for time (ITP ‘21).
Publications
All publications should either be gold open access (i.e. freely accessible via the publisher) or green open access (i.e. uploaded to a preprint 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.
 Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau, 2023. Verified Extraction from Coq to OCaml,
 Yannick Forster, Dominik Kirst, and Niklas Mück, 2024. The KleenePost and Post’s Theorem in the Calculus of Inductive Constructions, In: 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024, February 1923, 2024, Naples, Italy, LIPIcs, Schloss Dagstuhl  LeibnizZentrum für Informatik, pp. 29:1–29:20.
 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 2629, 2023, Proceedings, Lecture Notes in Computer Science, Springer, pp. 155–181.
 Matthieu Sozeau, Yannick Forster, Meven LennonBertrand, Jakob Botsch Nielsen, Nicolas Tabareau, and Théo Winterhalter, 2023. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq,
 Yannick Forster, Felix Jahn, and Gert Smolka, 2023. A Computational CantorBernstein 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.
 Yannick Forster and Felix Jahn, 2023. Constructive and Synthetic Reducibility Degrees: Post’s Problem for ManyOne and TruthTable Reducibility in Coq, In: 31st EACSL Annual Conference on Computer Science Logic, CSL 2023, February 1316, 2023, Warsaw, Poland, LIPIcs, Schloss Dagstuhl  LeibnizZentrum für Informatik, pp. 21:1–21:21.
 Yannick Forster, Fabian Kunze, and Nils Lauermann, 2022. Synthetic Kolmogorov Complexity in Coq, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 710, 2022, Haifa, Israel, volume 237, pp. 12:1–12:19.
 Yannick Forster, 2022. Parametric Church’s Thesis: Synthetic Computability Without Choice, In: Logical Foundations of Computer Science, Cham: Springer International Publishing, pp. 70–89.
 Yannick Forster, Fabian Kunze, Gert Smolka, and Maxi Wuttke, 2021. A Mechanised Proof of the Time Invariance Thesis for the Weak CallByValue \(λ\)Calculus, In: 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), LIPIcs, Schloss Dagstuhl  LeibnizZentrum für Informatik, pp. 19:1–19:20.
 Yannick Forster, Dominik Kirst, and Dominik Wehr, 2021. Completeness theorems for firstorder logic analysed in constructive type theory (extended version), J. Log. Comput., volume 31, number 1, pp. 112–151.
 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 2528, 2021, Ljubljana, Slovenia (Virtual Conference), LIPIcs, Schloss Dagstuhl  LeibnizZentrum für Informatik, pp. 21:1–21:19. (talk)
 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.
 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.
 Yannick Forster, Fabian Kunze, and Marc Roth, 2020. The weak callbyvalue λcalculus is reasonable for both time and space, Proc. ACM Program. Lang., volume 4, number POPL, pp. 27:1–27:23.
 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 2021, 2020, ACM, pp. 114–128.
 Simon Spies and Yannick Forster, 2020. Undecidability of higherorder 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 2021, 2020, ACM, pp. 143–157.
 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 2021, 2020, ACM, pp. 186–200.
 Yannick Forster, Dominik Kirst, and Dominik Wehr, 2020. Completeness Theorems for FirstOrder Logic Analysed in Constructive Type Theory, In: Logical Foundations of Computer Science  International Symposium, LFCS 2020, Deerfield Beach, FL, USA, January 47, 2020, Proceedings, Lecture Notes in Computer Science, Springer, pp. 47–74.
 Dominique LarcheyWendling and Yannick Forster, 2020. Hilbert’s Tenth Problem in Coq (extended version), CoRR, volume abs/2003.04604.
 Yannick Forster and Gert Smolka, 2019. CallbyValue Lambda Calculus as a Model of Computation in Coq, J. Autom. Reason., volume 63, number 2, pp. 393–413.
 Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar, 2019. On the expressive power of userdefined effects: Effect handlers, monadic reflection, delimited control, J. Funct. Program., volume 29, p. e15.
 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 1415, 2019, ACM, pp. 38–51.
 Yannick Forster and Dominique LarcheyWendling, 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 1415, 2019, ACM, pp. 104–117.
 Yannick Forster, Steven Schäfer, Simon Spies, and Kathrin Stark, 2019. Callbypushvalue 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 1415, 2019, ACM, pp. 118–131.
 Yannick Forster and Fabian Kunze, 2019. A Certifying Extraction with Time Bounds from Coq to CallByValue Lambda Calculus, In: 10th International Conference on Interactive Theorem Proving, ITP 2019, September 912, 2019, Portland, OR, USA, LIPIcs, Schloss Dagstuhl  LeibnizZentrum für Informatik, pp. 17:1–17:19.
 Dominique LarcheyWendling and Yannick Forster, 2019. Hilbert’s Tenth Problem in Coq, In: 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 2430, 2019, Dortmund, Germany, LIPIcs, Schloss Dagstuhl  LeibnizZentrum für Informatik, pp. 27:1–27:20.
 Fabian Kunze, Gert Smolka, and Yannick Forster, 2018. Formal SmallStep Verification of a CallbyValue Lambda Calculus Machine, In: Programming Languages and Systems  16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 26, 2018, Proceedings, Lecture Notes in Computer Science, Springer, pp. 264–283.
 Yannick Forster, Edith Heiter, and Gert Smolka, 2018. Verification of PCPRelated 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 912, 2018, Proceedings, Lecture Notes in Computer Science, Springer, pp. 253–269.
 Yannick Forster, Ohad Kammar, Sam Lindley, and Matija Pretnar, 2017. On the expressive power of userdefined effects: effect handlers, monadic reflection, delimited control, Proc. ACM Program. Lang., volume 1, number ICFP, pp. 13:1–13:29.
 Yannick Forster and Gert Smolka, 2017. Weak CallbyValue Lambda Calculus as a Model of Computation in Coq, In: Interactive Theorem Proving  8th International Conference, ITP 2017, Brası́lia, Brazil, September 2629, 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, PierreMarie 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 CantorBernstein 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 machinechecked intermediate language for extraction from Coq, in MetaCoq
Yannick Forster, Matthieu Sozeau
TYPES 2022, Nantes, France, 2022. 
Synthetic Versions of the KleenePost 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 LennonBertrand, 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 LarcheyWendling, 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 LarcheyWendling
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 LarcheyWendling
LOLA 2018, Oxford, UK, 2018. 
The strong invariance thesis for a lambdacalculus (slides)
Yannick Forster, Fabian Kunze, Marc Roth
LOLA 2017, Reykjavik, Iceland, 2017. 
Verified Extraction from Coq to a LambdaCalculus (slides)
Yannick Forster and Fabian Kunze
Coq Workshop 2016, ITP 2016, Nancy, France, 2016.
Talks
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, PierreMarie 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, PierreMarie 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, PierreMarie Pédrot, and Nicolas Tabareau.
Teaching
Supervised students
Haoyi Zeng, 2023, Bachelor's thesis, coadvised with Dominik Kirst
Post's problem and the priority method in the Calculus of Inductive Constructions
Janis Bailitis, 2024, Bachelor's thesis, coadvised with Dominik Kirst
Löb's theorem in Coq
Fabian Brenner, 2024, Bachelor's thesis, coadvised with Dominik Kirst
The undecidability of finitary PCF in Coq
Niklas Mück, 2021, Bachelor's thesis, coadvised 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 OneOne, ManyOne, and TruthTable Reducibility in Coq
Marcel Ullrich, 2020, Bachelor's thesis
Generating induction principles for nested inductive types in MetaCoq
Dominik Wehr, 2019, Bachelor's thesis, coadvised with Dominik Kirst
A Constructive Analysis of FirstOrder Completeness Theorems in Coq
Simon Spies, 2019, Bachelor's thesis
Formalising the Undecidability of HigherOrder Unification
Maxi Wuttke, 2018, Bachelor's thesis
Verified Programming Of Turing Machines In Coq
Edith Heiter, 2017, Bachelor's thesis, coadvised with Gert Smolka
Undecidability of the Post Correspondence Problem in Coq
Lectures
Winter 2023/2024  Lecturer Proof assistants M2 course, Parisian Master in Research in Computer Science (MPRI), with Théo Winterhalter. 
Winter 2023/2023  Lecturer Proof assistants M2 course, Parisian Master in Research in Computer Science (MPRI), with Matthieu Sozeau and Théo Winterhalter. 
Winter 2020/2021  Organiser and Lecturer Advanced Coq Programming Block course, Programming Systems Lab. 
Winter 2018/2019  TA Programming 1 Basic course, Programming Systems Lab. 
Summer 2018  Organiser and Lecturer Advanced Coq Programming Block course, Programming Systems Lab. 
Winter 2017  Adviser Category Theory Seminar, Programming Systems Lab. 
Summer 2017  Organiser Mathematics Precourse Saarland University. 
Summer 2017  Organiser Didactic Seminar for Student TAs in Programming 1 Reactive Systems Group. 
Summer 2017  TA Introduction to Computational Logic Core course, Programming Systems Lab. 
Summer 2017  Adviser Category Theory Seminar, Programming Systems Lab. 
Winter 2016  Adviser Funktionale Programmierung Proseminar, Programming Systems Lab. 
Summer 2016  Lecturer, Coach and Organiser Mathematics Precourse Saarland University. 
Summer 2015  Part of the organisation team Mathematics Precourse Saarland University. 
Winter 2014/2015  Organiser Didactic Seminar for Reexam Student TAs Reactive Systems Group. 
Winter 2014/2015  Supervision Student TA Programming 1 Basic course, Reactive Systems Group. 
Summer 2014  Student TA Introduction to Computational Logic Core course, Programming Systems Lab. 
Winter 2013/2014  Student TA Programming 1 Basic course, Dependendable Systems Group. 
Summer 2013  Student TA Mathematics Precourse Saarland University. 
Short CV
 since 2023: Permanent researcher (“chargé de recherche”) in the Cambium team at Inria Paris.
 20212023: Postdoctoral Marie SkłodowskaCurie 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.