## 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 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. I am also working on constructive formalisations of computability theory and undecidability proofs and I am interested in the theory and formalisation of computational effects. I obtained my Bachelor's degree at Saarland University and my Master's degree at the University of Cambridge. CV - Google Scholar - dblp - GitHub |

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

*Yannick Forster and Gert Smolka*

Journal of Automated Reasoning, 2018.

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

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

*Fabian Kunze, Gert Smolka, Yannick Forster*

Preprint, arxiv 1806.03205

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

*Yannick Forster, Edith Heiter, Gert Smolka*

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

**The strong invariance thesis for a lambda-calculus** *(slides)*

*Yannick Forster, Fabian Kunze, Marc Roth*

LOLA 2017, Reykjavik, Iceland, 2017.

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

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

Edith Heiter, 2017, Bachelor's thesis, co-supervised with Gert Smolka

Undecidability of the Post Correspondence Problem in Coq

Maximilian Wuttke, 2017, Bachelor's thesis

Formalising Turing machines in Coq

Simon Spies, 2018, Bachelor's thesis (ongoing)

Formalising the Undecidability of Higher-Order Unification

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 |