Yannick Forster

According to our database1, Yannick Forster authored at least 21 papers between 2017 and 2021.

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

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2021
Completeness theorems for first-order logic analysed in constructive type theory.
J. Log. Comput., 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...