Freek Wiedijk - RankMe

53 papers A 1B 4Misc 1Journal 21Unranked 20

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	A formalization of the Gelfond-Schneider theorem. CoRR Michail Karatarakis, Freek Wiedijk
2025	J	`jnl`	Formalized Hopfield Networks and Boltzmann Machines. CoRR Matteo Cipollina, Michail Karatarakis, Freek Wiedijk
2024	—	`ed.`	Logics and Type Systems in Theory and Practice - Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday Logics and Type Systems in Theory and Practice Venanzio Capretta, Robbert Krebbers, Freek Wiedijk
2021	A	`conf`	A Coq proof of the correctness of X25519 in TweetNaCl. CSF Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk
2021	J	`jnl`	A Coq proof of the correctness of X25519 in TweetNaCl. IACR Cryptol. ePrint Arch. Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk
2019	J	`jnl`	A benchmark for C program verification. CoRR Marko C. J. D. van Eekelen, Daniil Frumin, Herman Geuvers, Léon Gondelman, Robbert Krebbers, Marc Schoolderman, Sjaak Smetsers, Freek Verbeek, Benoît Viguier, Freek Wiedijk
2019	J	`jnl`	Proof-checking Euclid. Ann. Math. Artif. Intell. Michael Beeson, Julien Narboux, Freek Wiedijk
2017	J	`jnl`	Proof-checking Euclid. CoRR Michael Beeson, Julien Narboux, Freek Wiedijk
2016	J	`jnl`	A Probabilistic Analysis of the Game of the Goose. SIAM Rev. Jan Friso Groote, Freek Wiedijk, Hans Zantema
2016	J	`jnl`	Preface: Twenty Years of the QED Manifesto. J. Formaliz. Reason. John Harrison, Josef Urban, Freek Wiedijk
2015	B	`conf`	A Typed C11 Semantics for Interactive Theorem Proving. CPP Robbert Krebbers, Freek Wiedijk
2015	J	`jnl`	Foreword to the Special Focus on Formal Proofs for Mathematics and Computer Science. Math. Comput. Sci. Laurent Théry, Freek Wiedijk
2014	B	`conf`	Formal C Semantics: CompCert and the C Standard. ITP Robbert Krebbers, Xavier Leroy, Freek Wiedijk
2014	—	`ch.`	History of Interactive Theorem Proving. Computational Logic John Harrison, Josef Urban, Freek Wiedijk
2013	—	`conf`	Explicit convertibility proofs in pure type systems. LFMTP Floris van Doorn, Herman Geuvers, Freek Wiedijk
2013	B	`conf`	Separation Logic for Non-local Control Flow and Block Scope Variables. FoSSaCS Robbert Krebbers, Freek Wiedijk
2012	J	`jnl`	"Handbook of Practical Logic and Automated Reasoning, " by John R. Harrison, Cambridge University Press, 2009. J. Autom. Reason. Freek Wiedijk
2012	J	`jnl`	A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving Log. Methods Comput. Sci. Freek Wiedijk
2011	—	`conf`	A Formalization of the C99 Standard in HOL, Isabelle and Coq. Calculemus/MKM Robbert Krebbers, Freek Wiedijk
2011	B	`ed.`	Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings ITP Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, Freek Wiedijk
2010	—	`conf`	Pollack-inconsistency. UITP Freek Wiedijk
2010	J	`jnl`	Preface. J. Autom. Reason. Jacques Carette, Makarius Wenzel, Freek Wiedijk
2010	J	`jnl`	Proviola: A Tool for Proof Re-animation CoRR Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk
2010	—	`conf`	Proviola: A Tool for Proof Re-animation. AISC/MKM/Calculemus Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk
2010	—	`conf`	Pure Type Systems without Explicit Contexts LFMTP Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk
2009	—	`conf`	Stateless HOL TYPES Freek Wiedijk
2008	—	`conf`	A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers
2008	—	`ed.`	Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28 - August 1, 2008. Proceedings AISC/MKM/Calculemus Serge Autexier, John A. Campbell, Julio Rubio, Volker Sorge, Masakazu Suzuki, Freek Wiedijk
2008	—	`conf`	Merging Procedural and Declarative Proof. TYPES Cezary Kaliszyk, Freek Wiedijk
2007	—	`conf`	Certified Computer Algebra on Top of an Interactive Theorem Prover. Calculemus/MKM Cezary Kaliszyk, Freek Wiedijk
2007	J	`jnl`	Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk
2007	—	`conf`	Mizar's Soft Type System. TPHOLs Freek Wiedijk
2007	J	`jnl`	Preface to the special issue: Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. Bas Spitters, Herman Geuvers, Milad Niqui, Freek Wiedijk
2006	—	`ch.`	Introduction. The Seventeen Provers of the World Freek Wiedijk
2006	J	`jnl`	Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics. J. Appl. Log. Freek Wiedijk
2006	—	`book`	The Seventeen Provers of the World, Foreword by Dana S. Scott The Seventeen Provers of the World Freek Wiedijk
2005	J	`jnl`	The meaning of infinity in calculus and computer algebra systems. J. Symb. Comput. Michael Beeson, Freek Wiedijk
2004	—	`conf`	A Logical Framework with Explicit Conversions. LFM@IJCAR Herman Geuvers, Freek Wiedijk
2004	—	`conf`	C-CoRN, the Constructive Coq Repository at Nijmegen. MKM Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk
2004	—	`conf`	Hierarchical Reflection. TPHOLs Luís Cruz-Filipe, Freek Wiedijk
2003	—	`conf`	Comparing Mathematical Provers. MKM Freek Wiedijk
2003	—	`conf`	First Order Logic with Domain Conditions. TPHOLs Freek Wiedijk, Jan Zwanenburg
2003	—	`conf`	Formal Proof Sketches. TYPES Freek Wiedijk
2003	—	`ed.`	Types for Proofs and Programs, Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers TYPES Herman Geuvers, Freek Wiedijk
2002	J	`jnl`	A Comparison of Mizar and Isar. J. Autom. Reason. Markus Wenzel, Freek Wiedijk
2002	J	`jnl`	A Constructive Algebraic Hierarchy in Coq. J. Symb. Comput. Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg
2002	J	`jnl`	A New Implementation of Automath. J. Autom. Reason. Freek Wiedijk
2002	Misc	`conf`	The Meaning of Infinity in Calculus and Computer Algebra Systems. AISC Michael Beeson, Freek Wiedijk
2001	—	`conf`	Mizar Light for HOL Light. TPHOLs Freek Wiedijk
2000	—	`conf`	A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. TYPES Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
2000	—	`conf`	Equational Reasoning via Partial Reflection. TPHOLs Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
1991	J	`jnl`	Uniform Algebraic Specifications of Finite Sets with Equality. Int. J. Found. Comput. Sci. Jan A. Bergstra, Sjouke Mauw, Freek Wiedijk
1989	—	`conf`	Specification of the Transit Node in PSF Algebraic Methods Sjouke Mauw, Freek Wiedijk