Freek Wiedijk

According to our database, Freek Wiedijk authored at least 42 papers between 1989 and 2021.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2021

A Coq proof of the correctness of X25519 in TweetNaCl.

Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk

IACR Cryptol. ePrint Arch., 2021

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

Proof-checking Euclid.

Michael Beeson, Julien Narboux, Freek Wiedijk

Ann. Math. Artif. Intell., 2019

2016

A Probabilistic Analysis of the Game of the Goose.

Jan Friso Groote, Freek Wiedijk, Hans Zantema

SIAM Rev., 2016

Preface: Twenty Years of the QED Manifesto.

John Harrison, Josef Urban, Freek Wiedijk

J. Formaliz. Reason., 2016

2015

Foreword to the Special Focus on Formal Proofs for Mathematics and Computer Science.

Laurent Théry, Freek Wiedijk

Math. Comput. Sci., 2015

A Typed C11 Semantics for Interactive Theorem Proving.

Robbert Krebbers, Freek Wiedijk

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014

History of Interactive Theorem Proving.

John Harrison, Josef Urban, Freek Wiedijk

Proceedings of the Computational Logic, 2014

Formal C Semantics: CompCert and the C Standard.

Robbert Krebbers, Xavier Leroy, Freek Wiedijk

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013

Explicit convertibility proofs in pure type systems.

Floris van Doorn, Herman Geuvers, Freek Wiedijk

Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, 2013

Separation Logic for Non-local Control Flow and Block Scope Variables.

Robbert Krebbers, Freek Wiedijk

Proceedings of the Foundations of Software Science and Computation Structures, 2013

2012

"Handbook of Practical Logic and Automated Reasoning, " by John R. Harrison, Cambridge University Press, 2009.

Freek Wiedijk

J. Autom. Reason., 2012

A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving

Freek Wiedijk

Log. Methods Comput. Sci., 2012

2011

A Formalization of the C99 Standard in HOL, Isabelle and Coq.

Robbert Krebbers, Freek Wiedijk

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

2010

Preface.

Jacques Carette, Makarius Wenzel, Freek Wiedijk

J. Autom. Reason., 2010

Pollack-inconsistency.

Freek Wiedijk

Proceedings of the 9th International Workshop On User Interfaces for Theorem Provers, 2010

Pure Type Systems without Explicit Contexts

Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk

Proceedings of the Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2010

Proviola: A Tool for Proof Re-animation.

Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk

Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2009

Stateless HOL

Freek Wiedijk

Proceedings of the Proceedings Types for Proofs and Programs, Revised Selected Papers, 2009

2008

Merging Procedural and Declarative Proof.

Cezary Kaliszyk, Freek Wiedijk

Proceedings of the Types for Proofs and Programs, International Conference, 2008

A Real Semantic Web for Mathematics Deserves a Real Semantics.

Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, James McKinna, Herman Geuvers

Proceedings of the 3rd Semantic Wiki Workshop (SemWiki 2008) at the 5th European Semantic Web Conference (ESWC 2008), 2008

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

Constructive analysis, types and exact real numbers.

Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk

Math. Struct. Comput. Sci., 2007

Mizar's Soft Type System.

Freek Wiedijk

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

Certified Computer Algebra on Top of an Interactive Theorem Prover.

Cezary Kaliszyk, Freek Wiedijk

Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

2006

Is ZF a hack?: Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics.

Freek Wiedijk

J. Appl. Log., 2006

Introduction.

Freek Wiedijk

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

2005

The meaning of infinity in calculus and computer algebra systems.

Michael Beeson, Freek Wiedijk

J. Symb. Comput., 2005

2004

A Logical Framework with Explicit Conversions.

Herman Geuvers, Freek Wiedijk

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, 2004

Hierarchical Reflection.

Luís Cruz-Filipe, Freek Wiedijk

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

C-CoRN, the Constructive Coq Repository at Nijmegen.

Luís Cruz-Filipe, Herman Geuvers, Freek Wiedijk

Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

2003

Formal Proof Sketches.

Freek Wiedijk

Proceedings of the Types for Proofs and Programs, International Workshop, 2003

First Order Logic with Domain Conditions.

Freek Wiedijk, Jan Zwanenburg

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

Comparing Mathematical Provers.

Freek Wiedijk

Proceedings of the Mathematical Knowledge Management, Second International Conference, 2003

2002

A Constructive Algebraic Hierarchy in Coq.

Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg

J. Symb. Comput., 2002

A New Implementation of Automath.

Freek Wiedijk

J. Autom. Reason., 2002

A Comparison of Mizar and Isar.

Markus Wenzel, Freek Wiedijk

J. Autom. Reason., 2002

2001

Mizar Light for HOL Light.

Freek Wiedijk

Proceedings of the Theorem Proving in Higher Order Logics, 14th International Conference, 2001

2000

A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals.

Herman Geuvers, Freek Wiedijk, Jan Zwanenburg

Proceedings of the Types for Proofs and Programs, International Workshop, 2000

Equational Reasoning via Partial Reflection.

Herman Geuvers, Freek Wiedijk, Jan Zwanenburg

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

1991

Uniform Algebraic Specifications of Finite Sets with Equality.

Jan A. Bergstra, Sjouke Mauw, Freek Wiedijk

Int. J. Found. Comput. Sci., 1991

1989

Specification of the Transit Node in PSF_d.

Sjouke Mauw, Freek Wiedijk

Proceedings of the Algebraic Methods II: Theory, 1989