## About meI am a PhD student at the Saarbrücken Graduate School of Computer Science and the Programming Systems Lab under supervision of Gert Smolka. My research centers around analysing, formalising, and mechanising different aspects of computation in constructive type theory, and especially in the proof assistant Coq. One line of work is synthetic computability theory, where the fact that all definable functions in constructive type theory are computable is made explicit via axioms. We gave a general discussion of the axiom CT (Church's thesis) in relation to other axioms for Coq's type theory (CSL '21). A second line is formed by mechanising equivalence proofs between different models of computation. 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). The third line is formed by synthetic undecidability proofs. Since all functions definable in Coq's type theory are by definition computable, 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. Lastly, I am interested in using Coq as a system to obtain verified executable programs: I am involved in the MetaCoq project, a mechanisation and implementation of Coq in Coq, where I verified type and proof erasure (POPL '20), and in CertiCoq, a verified compiler for Coq. I obtained my Bachelor's degree at Saarland University and my Master's degree at the University of Cambridge. |

**A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value λ-Calculus** *(first draft) (doi) (cite)*

* Yannick Forster, Fabian Kunze, Gert Smolka, Maximilan Wuttke*

ITP 2021.

**Church’s thesis and related axioms in Coq’s type theory** *(pdf)* *(talk recording)* *(doi) (cite)*

* Yannick Forster*

CSL 2021, Ljubljana, Slovenia, 2021.

**Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)** *(pdf)* *(doi) (cite)*

* Yannick Forster, Dominik Kirst, Dominik Wehr*

Journal of Logic and Computation, Oxford University Press, 2021.

**Hilbert's Tenth Problem in Coq (extended version)** *(pdf)*

*Dominique Larchey-Wendling and Yannick Forster*

Submitted for review.

**Coq Coq Correct! - Verification of Type Checking and Erasure for Coq, in Coq** *(pdf)* *(doi) (cite)*

*Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau and Théo Winterhalter*

POPL 2020, New Orleans, USA, 2020.

**The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space** *(pdf) (slides)* *(doi) (cite)*

*Yannick Forster, Fabian Kunze, Marc Roth*

POPL 2020, New Orleans, USA, 2020.

**Coq à la Carte - A Practical Approach to Modular Syntax with Binders** *(pdf)* *(doi) (cite)*

* Yannick Forster and Kathrin Stark*

CPP 2020, New Orleans, USA, 2020.

**Verified Programming of Turing Machines in Coq** *(pdf)* *(doi) (cite)*

* Yannick Forster, Fabian Kunze, Maximilian Wuttke*

CPP 2020, New Orleans, USA, 2020.

**Undecidability of Higher-Order Unification Formalised in Coq** *(pdf) (slides)* *(doi) (cite)*

* Simon Spies and Yannick Forster*

CPP 2020, New Orleans, USA, 2020.

**Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory** *(pdf)* *(doi) (cite)*

* Yannick Forster, Dominik Kirst, Dominik Wehr*

Symposium on Logical Foundations Of Computer Science (LFCS 2020), January 4-7, 2020, Deerfield Beach, Florida, U.S.A.

**On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control (updated version)** *(pdf)* *(doi) (cite)*

*Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar*

Journal of Functional Programming Special Issue: Post-Proceedings of ICFP 2017, 2019.

Journal of Automated Reasoning, 2020.

**A certifying extraction with time bounds from Coq to call-by-value λ-calculus** *(pdf) (slides)* *(doi) (cite)*

*Yannick Forster and Fabian Kunze*

ITP 2019, Portland, USA, 2019. Pre-print on arxiv.

**Hilbert's Tenth Problem in Coq** *(pdf) (slides)* *(doi) (cite)*

*Dominique Larchey-Wendling and Yannick Forster*

FSCD 2019, Dortmund, Germany, 2019.

**Call-By-Push-Value in Coq: Operational, Equational and Denotational Theory** *(pdf) (slides)* *(doi) (cite)*

*Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark*

CPP 2019, Cascais, Portugal, 2019.

**On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem** *(pdf)* *(doi) (cite)*

*Yannick Forster, Dominik Kirst, Gert Smolka*

CPP 2019, Cascais, Portugal, 2019.

**Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines** *(pdf) (slides)* *(doi) (cite)*

*Yannick Forster and Dominique Larchey-Wendling*

CPP 2019, Cascais, Portugal, 2019.

**Formal Small-step Verification of a Call-by-value Lambda Calculus Machine** *(doi) (cite)*

*Fabian Kunze, Gert Smolka, Yannick Forster*

APLAS 2018, Wellington, New Zealand, 2018

**Call-by-Value Lambda Calculus as a Model of Computation in Coq** *(pdf)* *(doi) (cite)*

*Yannick Forster and Gert Smolka*

Journal of Automated Reasoning, 2018.

**Verification of PCP-Related Computational Reductions in Coq** *(slides)* *(doi) (cite)*

*Yannick Forster, Edith Heiter, Gert Smolka*

ITP 2018, Oxford, UK, 2018. Pre-print on arxiv.

**Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq** *(pdf)* *(slides)* *(doi) (cite)*

*Yannick Forster and Gert Smolka*

ITP 2017, Brasilia, Brazil, 2017.

** On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control**

ICFP 2017, Oxford, UK, 2017.

**Generating induction principles and subterm relations for inductive types using MetaCoq ** *(pdf) (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** *(pdf) (slides) (talk recording)*

*Yannick Forster, Dominique Larchey-Wendling, Andrej Dudenhefner, Edith Heiter, Dominik Kirst, Fabian Kunze, Gert Smolka, Simon Spies, Dominik Wehr, Maximilian Wuttke*

CoqPL 2020, New Orleans, USA, 2020.

**Coq Coq Codet! - Towards a Verified Toolchain for Coq in MetaCoq** *(pdf) (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** *(pdf) (slides)*

*Yannick Forster and Dominique Larchey-Wendling*

MLA 2019, Nancy, France, 2019.

**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** *(pdf)* *(slides)*

*Yannick Forster and Fabian Kunze*

Coq Workshop 2016, ITP 2016, Nancy, France, 2016.

**On the expressive power of effect handlers and monadic reflection** *(pdf)*

*Yannick Forster*

Master's Thesis, Robinson College, University of Cambridge, 2016.

**A Formal and Constructive Theory of Computation** *(pdf)*

*Yannick Forster*

Bachelor's Thesis, Programming Systems Lab, Saarland University, 2014.

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

Maximilian Wuttke, 2017, 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

Winter 2020/2021 | Organiser and Lecturer Advanced Coq Programming Block course, Programming Systems Lab. |

Winter 2018/2019 | TAProgramming 1Basic 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 | OrganiserDidactic 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 teamMathematics Precourse Saarland University. |

Winter 2014/2015 | OrganiserDidactic Seminar for Re-exam Student TAs Reactive Systems Group. |

Winter 2014/2015 | Supervision Student TAProgramming 1Basic course, Reactive Systems Group. |

Summer 2014 | Student TAIntroduction to Computational LogicCore course, Programming Systems Lab. |

Winter 2013/2014 | Student TAProgramming 1Basic course, Dependendable Systems Group. |

Summer 2013 | Student TAMathematics Precourse Saarland University. |

Mail: | forster at cs.uni-saarland.de |

Adress: | Saarland University, Saarland Informatics Campus E1 3, Rm 523 66123 Saarbrücken |

Phone: | +49 (0)681 / 302-5626 |