Yannick Forster

Registered user since Thu 4 May 2017

Name:Yannick Forster
Country:France
Affiliation:Inria
Personal website:https://yforster.de

Contributions

ICFP 2023 Workshops Co-Chair in Organizing Committee
CPP 2023 Committee Member in Program Committee within the CPP 2023-track
Author of A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl) within the CPP 2023-track
Unsound 2022 Author of MetaCoq as a tool to prevent future unsoundness in Coq within the Sources of Unsoundness in Verification-track
ML 2022 Author of Extraction to OCaml from Coq: Operational Correctness Verified in Coq within the ML-track
WITS 2022 Author of The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoq within the WITS 2022-track
CPP 2021 Session Chair of Logic, Set Theory, and Category Theory (part of CPP 2021)
Committee Member in Program Committee within the CPP 2021-track
CPP 2020 Author of Verified Programming of Turing Machines in Coq within the CPP 2020-track
Author of Undecidability of Higher-Order Unification Formalised in Coq within the CPP 2020-track
Author of Coq à la Carte - A Practical Approach to Modular Syntax with Binders within the CPP 2020-track
CoqPL 2020 Author of A Coq Library of Undecidable Problems within the CoqPL-track
POPL 2020 Author of Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq within the Research Papers-track
Author of The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space within the Research Papers-track
CPP 2019 Author of Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines within the CPP 2019-track
Author of On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem within the CPP 2019-track
Author of Call-By-Push-Value in Coq: Operational, Equational, and Denotational Theory within the CPP 2019-track
ICFP 2017 Author of On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control within the Research Papers-track