Specification of the Transit Node in PSFd. - Sjouke Mauw; Freek Wiedijk (Algebraic Methods, 1989)

Uniform Algebraic Specifications of Finite Sets with Equality. - Jan A. Bergstra; Sjouke Mauw; Freek Wiedijk (Int. J. Found. Comput. Sci., 1991)

Equational Reasoning via Partial Reflection. - Herman Geuvers; Freek Wiedijk; Jan Zwanenburg (TPHOLs, 2000)

A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. - Herman Geuvers; Freek Wiedijk; Jan Zwanenburg (TYPES, 2000)

Mizar Light for HOL Light. - Freek Wiedijk (TPHOLs, 2001)

A Comparison of Mizar and Isar. - Markus Wenzel 001; Freek Wiedijk (J. Autom. Reason., 2002)

A New Implementation of Automath. - Freek Wiedijk (J. Autom. Reason., 2002)

A Constructive Algebraic Hierarchy in Coq. - Herman Geuvers; Randy Pollack; Freek Wiedijk; Jan Zwanenburg (J. Symb. Comput., 2002)

Comparing Mathematical Provers. - Freek Wiedijk (MKM, 2003)

First Order Logic with Domain Conditions. - Freek Wiedijk; Jan Zwanenburg (TPHOLs, 2003)

Formal Proof Sketches. - Freek Wiedijk (TYPES, 2003)

C-CoRN, the Constructive Coq Repository at Nijmegen. - Luís Cruz-Filipe; Herman Geuvers; Freek Wiedijk (MKM, 2004)

Hierarchical Reflection. - Luís Cruz-Filipe; Freek Wiedijk (TPHOLs, 2004)

A Logical Framework with Explicit Conversions. - Herman Geuvers; Freek Wiedijk (LFM@IJCAR, 2004)

The meaning of infinity in calculus and computer algebra systems. - Michael Beeson; Freek Wiedijk (J. Symb. Comput., 2005)

Introduction. - Freek Wiedijk (The Seventeen Provers of the World, 2006)

Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics. - Freek Wiedijk (J. Appl. Log., 2006)

Certified Computer Algebra on Top of an Interactive Theorem Prover. - Cezary Kaliszyk; Freek Wiedijk (Calculemus/MKM, 2007)

Mizar's Soft Type System. - Freek Wiedijk (TPHOLs, 2007)

Constructive analysis, types and exact real numbers. - Herman Geuvers; Milad Niqui; Bas Spitters; Freek Wiedijk (Math. Struct. Comput. Sci., 2007)

Preface to the special issue: Constructive analysis, types and exact real numbers. - Bas Spitters; Herman Geuvers; Milad Niqui; Freek Wiedijk (Math. Struct. Comput. Sci., 2007)

A Real Semantic Web for Mathematics Deserves a Real Semantics. - Cezary Kaliszyk; Pierre Corbineau; Freek Wiedijk; James McKinna; Herman Geuvers (SemWiki, 2008)

Merging Procedural and Declarative Proof. - Cezary Kaliszyk; Freek Wiedijk (TYPES, 2008)

Stateless HOL - Freek Wiedijk (TYPES, 2009)

Proviola: A Tool for Proof Re-animation. - Carst Tankink; Herman Geuvers; James McKinna; Freek Wiedijk (AISC/MKM/Calculemus, 2010)

Pure Type Systems without Explicit Contexts - Herman Geuvers; Robbert Krebbers; James McKinna; Freek Wiedijk (LFMTP, 2010)

Pollack-inconsistency. - Freek Wiedijk (UITP, 2010)

Preface. - Jacques Carette; Makarius Wenzel; Freek Wiedijk (J. Autom. Reason., 2010)

A Formalization of the C99 Standard in HOL, Isabelle and Coq. - Robbert Krebbers; Freek Wiedijk (Calculemus/MKM, 2011)

A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving - Freek Wiedijk (Log. Methods Comput. Sci., 2012)

"Handbook of Practical Logic and Automated Reasoning, " by John R. Harrison, Cambridge University Press, 2009. - Freek Wiedijk (J. Autom. Reason., 2012)

Separation Logic for Non-local Control Flow and Block Scope Variables. - Robbert Krebbers; Freek Wiedijk (FoSSaCS, 2013)

Explicit convertibility proofs in pure type systems. - Floris van Doorn; Herman Geuvers; Freek Wiedijk (LFMTP, 2013)

Formal C Semantics: CompCert and the C Standard. - Robbert Krebbers; Xavier Leroy; Freek Wiedijk (ITP, 2014)

History of Interactive Theorem Proving. - John Harrison 001; Josef Urban; Freek Wiedijk (Computational Logic, 2014)

A Typed C11 Semantics for Interactive Theorem Proving. - Robbert Krebbers; Freek Wiedijk (CPP, 2015)

Foreword to the Special Focus on Formal Proofs for Mathematics and Computer Science. - Laurent Théry; Freek Wiedijk (Math. Comput. Sci., 2015)

Preface: Twenty Years of the QED Manifesto. - John Harrison 001; Josef Urban; Freek Wiedijk (J. Formaliz. Reason., 2016)

A Probabilistic Analysis of the Game of the Goose. - Jan Friso Groote; Freek Wiedijk; Hans Zantema (SIAM Rev., 2016)

Proof-checking Euclid. - Michael Beeson; Julien Narboux; Freek Wiedijk (Ann. Math. Artif. Intell., 2019)

A benchmark for C program verification. - 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 (CoRR, 2019)

A Coq proof of the correctness of X25519 in TweetNaCl. - Peter Schwabe; Benoît Viguier; Timmy Weerwag; Freek Wiedijk (IACR Cryptol. ePrint Arch., 2021)