Follow
Yannick Forster
Yannick Forster
Postdoc in the Gallinette Team at Inria Nantes
Verified email at inria.fr - Homepage
Title
Cited by
Cited by
Year
Coq coq correct! verification of type checking and erasure for coq, in coq
M Sozeau, S Boulier, Y Forster, N Tabareau, T Winterhalter
Proceedings of the ACM on Programming Languages 4 (POPL), 1-28, 2019
732019
The metacoq project
M Sozeau, A Anand, S Boulier, C Cohen, Y Forster, F Kunze, G Malecha, ...
Journal of automated reasoning 64 (5), 947-999, 2020
702020
On synthetic undecidability in Coq, with an application to the Entscheidungsproblem
Y Forster, D Kirst, G Smolka
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
662019
Weak call-by-value lambda calculus as a model of computation in Coq
Y Forster, G Smolka
International Conference on Interactive Theorem Proving, 189-206, 2017
472017
On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control
Y Forster, O Kammar, S Lindley, M Pretnar
Proceedings of the ACM on Programming Languages 1 (ICFP), 1-29, 2017
472017
Hilbert's Tenth Problem in Coq
D Larchey-Wendling, Y Forster
4th International Conference on Formal Structures for Computation and …, 2019
45*2019
A Coq library of undecidable problems
Y Forster, D Larchey-Wendling, A Dudenhefner, E Heiter, D Kirst, F Kunze, ...
CoqPL 2020 The Sixth International Workshop on Coq for Programming Languages, 2020
412020
A certifying extraction with time bounds from Coq to call-by-value -calculus
Y Forster, F Kunze
10th International Conference on Interactive Theorem Proving (ITP 2019), 17 …, 2019
372019
Verification of PCP-related computational reductions in Coq
Y Forster, E Heiter, G Smolka
International Conference on Interactive Theorem Proving, 253-269, 2018
322018
Certified undecidability of intuitionistic linear logic via binary stack machines and Minsky machines
Y Forster, D Larchey-Wendling
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
282019
On the expressive power of user-defined effects: Effect handlers, monadic reflection, delimited control
Y Forster, O Kammar, S Lindley, M Pretnar
Journal of Functional Programming 29, 2019
272019
The weak call-by-value λ-calculus is reasonable for both time and space
Y Forster, F Kunze, M Roth
Proceedings of the ACM on Programming Languages 4 (POPL), 1-23, 2019
242019
Completeness theorems for first-order logic analysed in constructive type theory: Extended version
Y Forster, D Kirst, D Wehr
Journal of Logic and Computation 31 (1), 112-151, 2021
232021
Verified programming of Turing machines in Coq
Y Forster, F Kunze, M Wuttke
Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020
182020
Completeness theorems for first-order logic analysed in constructive type theory
Y Forster, D Kirst, D Wehr
International Symposium on Logical Foundations of Computer Science, 47-74, 2020
172020
Verified extraction from Coq to a lambda-calculus
Y Forster, F Kunze
Coq Workshop 2016, 2016
162016
Church's thesis and related axioms in Coq's type theory
Y Forster
29th EACSL Annual Conference on Computer Science Logic (CSL 2021) 183, 21:1 …, 2020
132020
Undecidability of higher-order unification formalised in Coq
S Spies, Y Forster
Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020
132020
Call-by-value lambda calculus as a model of computation in Coq
Y Forster, G Smolka
Journal of Automated Reasoning 63 (2), 393-413, 2019
132019
Call-by-push-value in Coq: operational, equational, and denotational theory
Y Forster, S Schäfer, S Spies, K Stark
Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019
112019
The system can't perform the operation now. Try again later.
Articles 1–20