Yannick Forster

According to our database, Yannick Forster authored at least 32 papers between 2017 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Verified Extraction from Coq to OCaml.

Yannick Forster, Matthieu Sozeau, Nicolas Tabareau

Proc. ACM Program. Lang., 2024

Separating Markov's Principles.

Liron Cohen, Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva, Vincent Rahli

Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, 2024

The Kleene-Post and Post's Theorem in the Calculus of Inductive Constructions.

Yannick Forster, Dominik Kirst, Niklas Mück

Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, 2024

2023

Constructive and Synthetic Reducibility Degrees: Post's Problem for Many-One and Truth-Table Reducibility in Coq.

Yannick Forster, Felix Jahn

Proceedings of the 31st EACSL Annual Conference on Computer Science Logic, 2023

A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl).

Yannick Forster, Felix Jahn, Gert Smolka

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions.

Yannick Forster, Dominik Kirst, Niklas Mück

Proceedings of the Programming Languages and Systems - 21st Asian Symposium, 2023

2022

Hilbert's Tenth Problem in Coq (Extended Version).

Dominique Larchey-Wendling, Yannick Forster

Log. Methods Comput. Sci., 2022

Parametric Church's Thesis: Synthetic Computability Without Choice.

Yannick Forster

Proceedings of the Logical Foundations of Computer Science - International Symposium, 2022

Synthetic Kolmogorov Complexity in Coq.

Yannick Forster, Fabian Kunze, Nils Lauermann

Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021

Computability in constructive type theory.

Yannick Forster

PhD thesis, 2021

Completeness theorems for first-order logic analysed in constructive type theory.

Yannick Forster, Dominik Kirst, Dominik Wehr

J. Log. Comput., 2021

A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus.

Yannick Forster, Fabian Kunze, Gert Smolka, Maxi Wuttke

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

Church's Thesis and Related Axioms in Coq's Type Theory.

Yannick Forster

Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

2020

Coq Coq correct! verification of type checking and erasure for Coq, in Coq.

Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter

Proc. ACM Program. Lang., 2020

The weak call-by-value λ-calculus is reasonable for both time and space.

Yannick Forster, Fabian Kunze, Marc Roth

Proc. ACM Program. Lang., 2020

The MetaCoq Project.

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

J. Autom. Reason., 2020

Generating induction principles and subterm relations for inductive types using MetaCoq.

Bohdan Liesnikov, Marcel Ullrich, Yannick Forster

CoRR, 2020

Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version).

Yannick Forster, Dominik Kirst, Dominik Wehr

CoRR, 2020

Undecidability of higher-order unification formalised in Coq.

Simon Spies, Yannick Forster

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

Coq à la carte: a practical approach to modular syntax with binders.

Yannick Forster, Kathrin Stark

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

Verified programming of Turing machines in Coq.

Yannick Forster, Fabian Kunze, Maxi Wuttke

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019

Call-by-Value Lambda Calculus as a Model of Computation in Coq.

Yannick Forster, Gert Smolka

J. Autom. Reason., 2019

A certifying extraction with time bounds from Coq to call-by-value $λ$-calculus.

Yannick Forster, Fabian Kunze

CoRR, 2019

Hilbert's Tenth Problem in Coq.

Dominique Larchey-Wendling, Yannick Forster

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus.

Yannick Forster, Fabian Kunze

Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Call-by-push-value in coq: operational, equational, and denotational theory.

Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

Certified undecidability of intuitionistic linear logic via binary stack machines and minsky machines.

Yannick Forster, Dominique Larchey-Wendling

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

On synthetic undecidability in coq, with an application to the entscheidungsproblem.

Yannick Forster, Dominik Kirst, Gert Smolka

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

Verification of PCP-Related Computational Reductions in Coq.

Yannick Forster, Edith Heiter, Gert Smolka

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine.

Fabian Kunze, Gert Smolka, Yannick Forster

Proceedings of the Programming Languages and Systems - 16th Asian Symposium, 2018

2017

On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control.

Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar

Proc. ACM Program. Lang., 2017

Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq.

Yannick Forster, Gert Smolka

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017