Yannick Forster

Orcid: 0000-0002-8676-9819

Affiliations:
  • INRIA Nantes, France
  • Saarland University, Germany (former)
  • University of Cambridge, UK (former)


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

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Verified Extraction from Coq to OCaml.
Proc. ACM Program. Lang., 2024

Separating Markov's Principles.
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.
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.
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).
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.
Proceedings of the Programming Languages and Systems - 21st Asian Symposium, 2023

2022
Hilbert's Tenth Problem in Coq (Extended Version).
Log. Methods Comput. Sci., 2022

Parametric Church's Thesis: Synthetic Computability Without Choice.
Proceedings of the Logical Foundations of Computer Science - International Symposium, 2022

Synthetic Kolmogorov Complexity in Coq.
Proceedings of the 13th International Conference on Interactive Theorem Proving, 2022

2021
Computability in constructive type theory.
PhD thesis, 2021

Completeness theorems for first-order logic analysed in constructive type theory.
J. Log. Comput., 2021

A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus.
Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

Church's Thesis and Related Axioms in Coq's Type Theory.
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.
Proc. ACM Program. Lang., 2020

The weak call-by-value λ-calculus is reasonable for both time and space.
Proc. ACM Program. Lang., 2020

The MetaCoq Project.
J. Autom. Reason., 2020

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

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

Undecidability of higher-order unification formalised in Coq.
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.
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

Verified programming of Turing machines in Coq.
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.
J. Autom. Reason., 2019

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

Hilbert's Tenth Problem in Coq.
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.
Proceedings of the 10th International Conference on Interactive Theorem Proving, 2019

Call-by-push-value in coq: operational, equational, and denotational theory.
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.
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.
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018
Verification of PCP-Related Computational Reductions in Coq.
Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine.
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.
Proc. ACM Program. Lang., 2017

Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq.
Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017


  Loading...