Yannick Forster

Saarland University Computer Science

About me

I 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

Yannick Forster

Publications

Full papers

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, to appear.

Coq Coq Correct! - Verification of Type Checking and Erasure for Coq, in Coq (pdf)
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau and Théo Winterhalter
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)
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

Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar
ICFP 2017, Oxford, UK, 2017.

Extended abstracts and talks

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.

Theses

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.

Supervised Students

Robert Schenck, 2019, Master's thesis (ongoing), co-advised with Fabian Kunze
Parametricity Proofs in Coq

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

Teaching

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 Re-exam 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.

Contact

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


Legal notice, Privacy policy