Yannick Forster

Cited by

	All	Since 2020
Citations	1140	990
h-index	18	18
i10-index	28	26

260

130

195

2017201820192020202120222023202420258 33 103 147 201 260 152 184 45

Public access

View all

15 articles

0 articles

available

not available

Based on funding mandates

Co-authors

Dominik KirstMSCA Postdoctoral Fellow, Inria ParisVerified email at inria.fr
Gert SmolkaProfessor of Computer Science, Saarland University, Saarland Informatics CampusVerified email at ps.uni-saarland.de
nicolas tabareauInriaVerified email at inria.fr
Matthieu SozeauResarcher, Inria Paris and PPSVerified email at inria.fr
Théo WinterhalterInria SaclayVerified email at inria.fr
Dominique Larchey-WendlingResearcher, LORIA, CNRSVerified email at loria.fr
Matija PretnarUniversity of Ljubljana, Faculty of Mathematics and PhysicsVerified email at fmf.uni-lj.si
Sam LindleyThe University of EdinburghVerified email at ed.ac.uk
Ohad KammarUniversity of Edinburgh School of InformaticsVerified email at ed.ac.uk
Simon SpiesMPI-SWSVerified email at mpi-sws.org
Edith HeiterPhD student at Ghent UniversityVerified email at ugent.be
Andrej DudenhefnerDepartment of Computer Science, TU Dortmund University, GermanyVerified email at cs.tu-dortmund.de
Felix JahnPh.D. Student, German Research Center for Artificial Intelligence (DFKI)Verified email at uni-saarland.de
Gregory MalechaBedRock Systems, IncVerified email at bedrocksystems.com
Marc RothSchool of Electronic Engineering and Computer Science, Queen Mary University of LondonVerified email at qmul.ac.uk
Kathrin StarkAssistant Professor, Heriot-Watt UniversityVerified email at hw.ac.uk
Vincent RahliUniversity of BirminghamVerified email at bham.ac.uk
Steven SchäferPhD student at the Programming Systems Lab, Saarland UniversityVerified email at ps.uni-saarland.de
Johannes HostertDoctoral Student, ETH ZurichVerified email at ethz.ch
Mark KochR&D Scientist at QuantinuumVerified email at quantinuum.com

Yannick Forster

Cambium Team, Inria Paris

Verified email at inria.fr - Homepage

Type Theory Constructive Mathematics Interactive Theorem Proving Programming Languages


Title Sort by citations Sort by year Sort by title	Cited by Cited by	Year
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	134	2020
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	125	2019
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	84	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	61	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	59	2017
Hilbert's Tenth Problem in Coq D Larchey-Wendling, Y Forster 4th International Conference on Formal Structures for Computation and …, 2019	58*	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	48	2020
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	44	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	42	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	40	2021
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	37	2018
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	35	2019
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	33	2019
Computability in constructive type theory Y Forster Saarländische Universitäts-und Landesbibliothek, 2021	29	2021
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	26	2020
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	26	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	25	2020
Parametric Church’s Thesis: Synthetic computability without choice Y Forster International Symposium on Logical Foundations of Computer Science, 70-89, 2021	20	2021
Undecidability of higher-order unification formalised in Coq S Spies, Y Forster Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020	18	2020
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	16	2020

The system can't perform the operation now. Try again later.

Articles 1–20

Citations per year

Duplicate citations

Merged citations

Add co-authorsCo-authors

Follow

Cited by

Co-authors