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
81 2019 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
77 2020 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
67 2019 Weak call-by-value lambda calculus as a model of computation in Coq Y Forster, G Smolka
Interactive Theorem Proving: 8th International Conference, ITP 2017 …, 2017
48 2017 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
47 2017 Hilbert's Tenth Problem in Coq D Larchey-Wendling, Y Forster
4th International Conference on Formal Structures for Computation and …, 2019
46 * 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
41 2020 A certifying extraction with time bounds from Coq to call-by-value Y Forster, F Kunze
10th International Conference on Interactive Theorem Proving (ITP 2019), 17 …, 2019
37 2019 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
31 2019 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
31 2018 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
28 2019 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
25 2021 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
25 2019 Verified programming of Turing machines in Coq Y Forster, F Kunze, M Wuttke
Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020
19 2020 Verified extraction from Coq to a lambda-calculus Y Forster, F Kunze
Coq Workshop 2016, 2016
17 2016 Completeness theorems for first-order logic analysed in constructive type theory Y Forster, D Kirst, D Wehr
Logical Foundations of Computer Science: International Symposium, LFCS 2020 …, 2020
16 2020 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
15 2020 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
13 2019 Parametric church’s thesis: Synthetic computability without choice Y Forster
Logical Foundations of Computer Science: International Symposium, LFCS 2022 …, 2021
12 2021 Undecidability of higher-order unification formalised in Coq S Spies, Y Forster
Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020
12 2020 
Gert SmolkaProfessor of Computer Science, Saarland University, Saarland Informatics CampusBestätigte E-Mail-Adresse bei ps.uni-saarland.de
