Freek Wiedijk

Publication Activity (10 Years)

Years Active: 1989-2021
Publications (10 Years): 9

Top Topics

Theorem Proving

Benchmark Suite

Mathematics And Computer Science

Top Venues

Math. Comput. Sci.

Ann. Math. Artif. Intell.

Publications

Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk
A Coq proof of the correctness of X25519 in TweetNaCl. CSF (2021)
Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk
A Coq proof of the correctness of X25519 in TweetNaCl. IACR Cryptol. ePrint Arch. 2021 (2021)
Michael Beeson, Julien Narboux, Freek Wiedijk
Proof-checking Euclid. Ann. Math. Artif. Intell. 85 (2-4) (2019)
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
A benchmark for C program verification. CoRR (2019)
Michael Beeson, Julien Narboux, Freek Wiedijk
Proof-checking Euclid. CoRR (2017)
John Harrison, Josef Urban, Freek Wiedijk
Preface: Twenty Years of the QED Manifesto. J. Formaliz. Reason. 9 (1) (2016)
Jan Friso Groote, Freek Wiedijk, Hans Zantema
A Probabilistic Analysis of the Game of the Goose. SIAM Rev. 58 (1) (2016)
Laurent Théry, Freek Wiedijk
Foreword to the Special Focus on Formal Proofs for Mathematics and Computer Science. Math. Comput. Sci. 9 (1) (2015)
Robbert Krebbers, Freek Wiedijk
A Typed C11 Semantics for Interactive Theorem Proving. CPP (2015)
Robbert Krebbers, Xavier Leroy, Freek Wiedijk
Formal C Semantics: CompCert and the C Standard. ITP (2014)
Robbert Krebbers, Freek Wiedijk
Separation Logic for Non-local Control Flow and Block Scope Variables. FoSSaCS (2013)
Floris van Doorn, Herman Geuvers, Freek Wiedijk
Explicit convertibility proofs in pure type systems. LFMTP (2013)
Freek Wiedijk
A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving Log. Methods Comput. Sci. 8 (1) (2012)
Freek Wiedijk
"Handbook of Practical Logic and Automated Reasoning, " by John R. Harrison, Cambridge University Press, 2009. J. Autom. Reason. 49 (1) (2012)
Freek Wiedijk
Pollack-inconsistency. Electron. Notes Theor. Comput. Sci. 285 (2012)
Robbert Krebbers, Freek Wiedijk
A Formalization of the C99 Standard in HOL, Isabelle and Coq. Calculemus/MKM (2011)
Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk
Proviola: A Tool for Proof Re-animation. AISC/MKM/Calculemus (2010)
Jacques Carette, Makarius Wenzel, Freek Wiedijk
Preface. J. Autom. Reason. 44 (1-2) (2010)
Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk
Proviola: A Tool for Proof Re-animation CoRR (2010)
Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk
Pure Type Systems without Explicit Contexts LFMTP (2010)
Freek Wiedijk
Stateless HOL TYPES (2009)
Herman Geuvers, Freek Wiedijk
A Logical Framework with Explicit Conversions. Electron. Notes Theor. Comput. Sci. 199 (2008)
Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers
A Real Semantic Web for Mathematics Deserves a Real Semantics. SemWiki (2008)
Cezary Kaliszyk, Freek Wiedijk
Merging Procedural and Declarative Proof. TYPES (2008)
Bas Spitters, Herman Geuvers, Milad Niqui, Freek Wiedijk
Preface to the special issue: Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17 (1) (2007)
Freek Wiedijk
Mizar's Soft Type System. TPHOLs (2007)
Cezary Kaliszyk, Freek Wiedijk
Certified Computer Algebra on Top of an Interactive Theorem Prover. Calculemus/MKM (2007)
Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk
Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17 (1) (2007)
Freek Wiedijk
Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics. J. Appl. Log. 4 (4) (2006)
Michael Beeson, Freek Wiedijk
The meaning of infinity in calculus and computer algebra systems. J. Symb. Comput. 39 (5) (2005)
Luís Cruz-Filipe, Freek Wiedijk
Hierarchical Reflection. TPHOLs (2004)
Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk
C-CoRN, the Constructive Coq Repository at Nijmegen. MKM (2004)
Freek Wiedijk
Comparing Mathematical Provers. MKM (2003)
Freek Wiedijk
Formal Proof Sketches. TYPES (2003)
Freek Wiedijk, Jan Zwanenburg
First Order Logic with Domain Conditions. TPHOLs (2003)
Michael Beeson, Freek Wiedijk
The Meaning of Infinity in Calculus and Computer Algebra Systems. AISC (2002)
Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg
A Constructive Algebraic Hierarchy in Coq. J. Symb. Comput. 34 (4) (2002)
Markus Wenzel, Freek Wiedijk
A Comparison of Mizar and Isar. J. Autom. Reason. 29 (3-4) (2002)
Freek Wiedijk
A New Implementation of Automath. J. Autom. Reason. 29 (3-4) (2002)
Freek Wiedijk
Mizar Light for HOL Light. TPHOLs (2001)
Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. TYPES (2000)
Herman Geuvers, Freek Wiedijk, Jan Zwanenburg
Equational Reasoning via Partial Reflection. TPHOLs (2000)
Jan A. Bergstra, Sjouke Mauw, Freek Wiedijk
Uniform Algebraic Specifications of Finite Sets with Equality. Int. J. Found. Comput. Sci. 2 (1) (1991)
Sjouke Mauw, Freek Wiedijk
. Algebraic Methods (1989)