Yannick Forster

Publication Activity (10 Years)

Years Active: 2016-2024
Publications (10 Years): 41

Top Topics

Quantifier Free

Datalog Queries

Lambda Calculus

Top Venues

Proc. ACM Program. Lang.

Publications

Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli
Separating Markov's Principles. LICS (2024)
Yannick Forster, Matthieu Sozeau, Nicolas Tabareau
Verified Extraction from Coq to OCaml. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Yannick Forster, Dominik Kirst, Niklas Mück
The Kleene-Post and Post's Theorem in the Calculus of Inductive Constructions. CSL (2024)
Yannick Forster, Dominik Kirst, Niklas Mück
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions. CoRR (2023)
Yannick Forster, Dominik Kirst, Niklas Mück
Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions. APLAS (2023)
Yannick Forster, Felix Jahn
Constructive and Synthetic Reducibility Degrees: Post's Problem for Many-One and Truth-Table Reducibility in Coq. CSL (2023)
Yannick Forster, Felix Jahn, Gert Smolka
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). CPP (2023)
Yannick Forster, Fabian Kunze, Nils Lauermann
Synthetic Kolmogorov Complexity in Coq. ITP (2022)
Dominique Larchey-Wendling, Yannick Forster
Hilbert's Tenth Problem in Coq (Extended Version). Log. Methods Comput. Sci. 18 (1) (2022)
Yannick Forster
Parametric Church's Thesis: Synthetic Computability Without Choice. LFCS (2022)
Yannick Forster
Church's Thesis and Related Axioms in Coq's Type Theory. CSL (2021)
Yannick Forster, Dominik Kirst, Dominik Wehr
Completeness theorems for first-order logic analysed in constructive type theory. J. Log. Comput. 31 (1) (2021)
Yannick Forster, Fabian Kunze, Gert Smolka, Maximilian Wuttke
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. ITP (2021)
Yannick Forster
Parametric Church's Thesis: Synthetic Computability without Choice. CoRR (2021)
Simon Spies, Yannick Forster
Undecidability of higher-order unification formalised in Coq. CPP (2020)
Yannick Forster, Dominik Kirst, Dominik Wehr
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version). CoRR (2020)
Bohdan Liesnikov, Marcel Ullrich, Yannick Forster
Generating induction principles and subterm relations for inductive types using MetaCoq. CoRR (2020)
Yannick Forster, Kathrin Stark
Coq à la carte: a practical approach to modular syntax with binders. CPP (2020)
Dominique Larchey-Wendling, Yannick Forster
Hilbert's Tenth Problem in Coq. CoRR (2020)
Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo Winterhalter
The MetaCoq Project. J. Autom. Reason. 64 (5) (2020)
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter
Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proc. ACM Program. Lang. 4 (POPL) (2020)
Yannick Forster, Fabian Kunze, Marc Roth
The weak call-by-value λ-calculus is reasonable for both time and space. Proc. ACM Program. Lang. 4 (POPL) (2020)
Yannick Forster, Fabian Kunze, Maximilian Wuttke
Verified programming of Turing machines in Coq. CPP (2020)
Yannick Forster, Dominik Kirst, Dominik Wehr
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory. LFCS (2020)
Yannick Forster
Church's thesis and related axioms in Coq's type theory. CoRR (2020)
Yannick Forster, Fabian Kunze, Marc Roth
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space. CoRR (2019)
Yannick Forster, Dominique Larchey-Wendling
Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines. CPP (2019)
Dominique Larchey-Wendling, Yannick Forster
Hilbert's Tenth Problem in Coq. FSCD (2019)
Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark
Call-by-push-value in coq: operational, equational, and denotational theory. CPP (2019)
Yannick Forster, Fabian Kunze
A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. ITP (2019)
Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar
On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control. J. Funct. Program. 29 (2019)
Yannick Forster, Dominik Kirst, Gert Smolka
On synthetic undecidability in coq, with an application to the entscheidungsproblem. CPP (2019)
Yannick Forster, Fabian Kunze
A certifying extraction with time bounds from Coq to call-by-value $λ$-calculus. CoRR (2019)
Yannick Forster, Gert Smolka
Call-by-Value Lambda Calculus as a Model of Computation in Coq. J. Autom. Reason. 63 (2) (2019)
Fabian Kunze, Gert Smolka, Yannick Forster
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine. CoRR (2018)
Yannick Forster, Edith Heiter, Gert Smolka
Verification of PCP-Related Computational Reductions in Coq. ITP (2018)
Fabian Kunze, Gert Smolka, Yannick Forster
Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. APLAS (2018)
Yannick Forster, Gert Smolka
Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. ITP (2017)
Yannick Forster, Edith Heiter, Gert Smolka
Verification of PCP-Related Computational Reductions in Coq. CoRR (2017)
Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar
On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar
On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control. CoRR (2016)