Seguir
Yannick Forster
Yannick Forster
Cambium Team, Inria Paris
Dirección de correo verificada de inria.fr - Página principal
Título
Citado por
Citado por
Año
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
1112019
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
1072020
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
762019
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
542017
Hilbert's Tenth Problem in Coq
D Larchey-Wendling, Y Forster
4th International Conference on Formal Structures for Computation and …, 2019
52*2019
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
512017
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
452020
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
412019
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, e15, 2019
382019
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
342021
Verification of PCP-related computational reductions in Coq
Y Forster, E Heiter, G Smolka
Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as …, 2018
342018
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
312019
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
282019
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, 2019
242019
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
232020
Verified programming of Turing machines in Coq
Y Forster, F Kunze, M Wuttke
Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020
212020
Parametric Church’s Thesis: Synthetic computability without choice
Y Forster
International Symposium on Logical Foundations of Computer Science, 70-89, 2021
172021
Verified extraction from Coq to a lambda-calculus
Y Forster, F Kunze
Coq Workshop 2016, 2016
172016
Coq à la carte: a practical approach to modular syntax with binders
Y Forster, K Stark
Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020
162020
Undecidability of higher-order unification formalised in Coq
S Spies, Y Forster
Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020
142020
El sistema no puede realizar la operación en estos momentos. Inténtalo de nuevo más tarde.
Artículos 1–20