## 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. I am working on a library of undecidable problems for the proof assistant Coq and on constructive formalisations of computability theory. I am also working on the strong invariance thesis for the call-by-value lambda calculus with the long-term goal of using this calculus as a formal basis for complexity theory and I am interested in the theory and formalisation of computational effects. Finally, I am contributing to MetaCoq and CertiCoq. I obtained my Bachelor's degree at Saarland University and my Master's degree at the University of Cambridge. CV - Google Scholar - dblp - GitHub |

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

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

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

* Yannick Forster and Kathrin Stark*

submitted for review, 2019.

**Verified Programming of Turing-Machines in Coq** *(pdf)*

* Yannick Forster, Fabian Kunze, Maximilian Wuttke*

submitted for review, 2019.

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

* Simon Spies and Yannick Forster*

submitted for review, 2019.

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

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

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

Submitted for review.

**The MetaCoq Project** *(pdf)*

*Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter*

hal-02167423, submitted for review, 2019.

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

*Yannick Forster and Fabian Kunze*

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

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

*Yannick Forster, Fabian Kunze, Marc Roth*

arxiv 1902.07515, submitted for review, 2019.

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

*Dominique Larchey-Wendling and Yannick Forster*

FSCD 2019, Dortmund, Germany, 2019.

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

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

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

*Yannick Forster and Dominique Larchey-Wendling*

CPP 2019, Cascais, Portugal, 2019.

** Formal Small-step Verification of a Call-by-value Lambda Calculus Machine**

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

*Yannick Forster and Gert Smolka*

Journal of Automated Reasoning, 2018.

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

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

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

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

Marcel Ullrich, 2019, Bachelor's thesis (ongoing)

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 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 ps.uni-saarland.de |

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

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