Constructive and Synthetic Reducibility Degrees: Post’s Problem for Many-one and Truth-table Reducibility in Coq
(pdf)
Yannick Forster, Felix Jahn
Computer Science Logic (CSL'23), Warsaw, Poland
A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory
(pdf)
Yannick Forster, Felix Jahn, Gert Smolka
CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory: Extended Version
(pdf)
Yannick Forster, Dominik Kirst, Dominik Wehr
Journal of Logic and Computation
Computability in Constructive Type Theory
Yannick Forster
PhD Thesis, Saarland University
A Mechanised Proof of the Time Invariance Thesis for the Weak Call-by-value λ-Calculus
(pdf)
Yannick Forster, Fabian Kunze, Gert Smolka, Maximilian Wuttke
12th International Conference on Interactive Theorem Proving (ITP 2021)
Church’s Thesis and Related Axioms in Coq’s Type Theory
(pdf)
Yannick Forster
29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq
(pdf)
Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, Théo Winterhalter
47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020), New Orleans, USA
Verified Programming of Turing Machines in Coq
(pdf)
Yannick Forster, Fabian Kunze, Maximilian Wuttke
9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20–21, 2020
Coq à la Carte - A Practical Approach to Modular Syntax with Binders
(pdf)
Yannick Forster, Kathrin Stark
9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, USA
Undecidability of Higher-Order Unification Formalised in Coq
(pdf)
Simon Spies, Yannick Forster
9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, USA
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory
(pdf)
Yannick Forster, Dominik Kirst, Dominik Wehr
Symposium on Logical Foundations Of Computer Science (LFCS 2020), January 4-7, 2020, Deerfield Beach, Florida, U.S.A.
The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space
(pdf)
Yannick Forster, Fabian Kunze, Marc Roth
47th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2020), New Orleans, USA
A certifying extraction with time bounds from Coq to call-by-value λ-calculus
(pdf)
Yannick Forster, Fabian Kunze
Interactive Theorem Proving - 10th International Conference, ITP 2019, Portland, USA
Hilbert's Tenth Problem in Coq
(pdf)
Dominique Larchey-Wendling, Yannick Forster
4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, Dortmund, Germany
Call-By-Push-Value in Coq: Operational, Equational and Denotational Theory
(pdf)
Yannick Forster, Steven Schäfer, Simon Spies, Kathrin Stark
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019
On Synthetic Undecidability in Coq, with an Application to the Entscheidungsproblem
(pdf)
Yannick Forster, Dominik Kirst, Gert Smolka
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019
Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines
(pdf)
Yannick Forster, Dominique Larchey-Wendling
8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019
Call-by-Value Lambda Calculus as a Model of Computation in Coq
(pdf)
Yannick Forster, Gert Smolka
Journal of Automated Reasoning
Formal Small-step Verification of a Call-by-value Lambda Calculus Machine
(pdf)
Fabian Kunze, Gert Smolka, Yannick Forster
16th Asian Symposium on Programming Languages and Systems, APLAS 2018, Wellington, New Zealand, December 2-6
Verification of PCP-Related Computational Reductions in Coq
(pdf)
Yannick Forster, Edith Heiter, Gert Smolka
Interactive Theorem Proving - 9th International Conference, ITP 2018, Oxford, UK, July 9-12, 2018
On the Expressive Power of User-Defined Effects: Effect Handlers, Monadic Reflection, Delimited Control
(pdf)
Yannick Forster, Ohad Kammar, Sam Lindley, Matija Pretnar
International Conference on Functional Programming, ICFP 2017, Oxford, United Kingdom, September 3-9, 2017
Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq
(pdf)
Yannick Forster, Gert Smolka
Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017