
W. Bosma, H. Jager & F. Wiedijk, "Some metrical observations on the approximation by continued fractions." Indag. Math. 45, 281299, 1983.

F. Wiedijk, Conforme supergravitatie zonder constraints. M.Sc. thesis (in Dutch), University of Amsterdam, 1986: djvu pdf cbr tar.gz

J.A. Bergstra, S. Mauw & F. Wiedijk, "Uniform algebraic specifications of finite sets with equality." Int. J. of Foundations of Computer Science 1(2), 4365, 1991.

S. Mauw & F. Wiedijk, "Specification of the transit node in PSFd." In: J.A. Bergstra & L.M.G. Feijs (eds.), Algebraic Methods II: Theory, Tools and Applications, Springer LNCS 490, 341361, 1991.

F. Wiedijk, Persistence in Algebraic Specifications. Ph.D. thesis, University of Amsterdam, 204 pp., 1991: ps.gz pdf

H. Geuvers, F. Wiedijk & J. Zwanenburg, "Equational Reasoning via Partial Reflection." In: John Harrison & Mark Aagaard, Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, Springer LNCS 1869, 162178, 2000:
ps.gz pdf dvi tex
Abstract.
We modify the reflection method to enable it to deal with partial functions like division. The idea behind reflection is to program a tactic for a theorem prover not in the implementation language but in the object language of the theorem prover itself. The main ingredients of the reflection method are a syntactic encoding of a class of problems, an interpretation function (mapping the encoding to the problem) and a decision function, written on the encodings. Together with a correctness proof of the decision function, this gives a fast method for solving problems. The contribution of this work lies in the extension of the reflection method to deal with equations in algebraic structures where some functions may be partial. The primary example here is the theory of fields. For the reflection method, this yields the problem that the interpretation function is not total. In this paper we show how this can be overcome by defining the interpretation as a relation. We give the precise details, both in mathematical terms and in Coq syntax. It has been used to program our own tactic "Rational", for verifying equations between field elements. [17 pp.]

F. Wiedijk, "Mizar Light for HOL Light". In: Richard Boulton & Paul Jackson (eds.), Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Springer LNCS 2152, 378393, 2001: ps.gz pdf dvi tex
Abstract.
There are two different approaches to formalizing proofs in a computer: the procedural approach (which is the one of the HOL system) and the declarative approach (which is the one of the Mizar system). Most provers are procedural. However declarative proofs are much closer in style to informal mathematical reasoning than procedural ones.
There have been attempts to put declarative interfaces on top of procedural proof assistants, like John Harrison's Mizar mode for HOL and Markus Wenzel's Isar mode for Isabelle. However in those cases the declarative assistant is a layer on top of the procedural basis, having a separate syntax and a different "feel" from the underlying system.
This paper shows that the procedural and the declarative ways of proving are related and can be integrated seamlessly. It presents an implementation of the Mizar proof language on top of HOL that consists of only 41 lines of ML. This shows how close the procedural and declarative styles of proving really are. [16 pp.]

H. Geuvers, F. Wiedijk & J. Zwanenburg, "A Constructive Proof of the Fundamental Theorem of Algebra without using the Rationals." In: Paul Callaghan, Zhaohui Luo, James McKinna & Robert Pollack (eds.), Types for Proofs and Programs, Proceedings of the International Workshop, TYPES 2000, Durham, Springer LNCS 2277, 96111, 2001: ps.gz pdf dvi tex
Abstract.
In the FTA project in Nijmegen we have formalized a constructive proof of the Fundamental Theorem of Algebra. In the formalization, we have first defined the (constructive) algebraic hierarchy of groups, rings, fields, etcetera. For the reals we have then defined the notion of real number structure, which is basically a Cauchy complete Archimedean ordered field. This boils down to axiomatizing the constructive reals. The proof of FTA is then given from these axioms (so independent of a specific construction of the reals), where the complex numbers are defined as pairs of real numbers.
The proof of FTA that we have chosen to formalize is the one in the seminal book by Troelstra and van Dalen, originally due to Manfred Kneser. The proof by Troelstra and van Dalen makes heavy use of the rational numbers (as suitable approximations of reals), which is quite common in constructive analysis, because equality on the rationals is decidable and equality on the reals isn't. In our case, this is not so convenient, because the axiomatization of the reals doesn't "contain" the rationals. Moreover, we found it rather unnatural to let a proof about the reals be mainly dealing with rationals. Therefore, our version of the FTA proof doesn't refer to the rational numbers. The proof described here is a faithful presentation of a fully formalized proof in the Coq system. [16 pp.]

H. Geuvers, R. Pollack, F. Wiedijk & J. Zwanenburg, "A Constructive Algebraic Hierarchy in Coq." In: S. Linton & R. Sebasitani (eds.), Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems, 34(4), Elsevier, 271286, 2002: ps.gz pdf dvi tex
Abstract.
We describe a framework of algebraic structures in the proof
assistant Coq. We have developed this framework as part of the FTA
project in Nijmegen, in which a constructive proof of the Fundamental
Theorem of Algebra has been formalized in Coq.
The algebraic hierarchy that is described here is both abstract and
structured. Structures like groups and rings are part of it in
an abstract way, defining e.g. a ring as a tuple consisting of a
group, a binary operation and a constant that together satisfy the
properties of a ring. In this way, a ring automatically inherits the
group properties of the additive subgroup. The algebraic hierarchy is
formalized in Coq by applying a combination of labelled record types
and coercions. In the labelled record types of Coq, one can use dependent types: the type of one label may depend on another
label. This allows to give a type to a dependenttyped tuple like
<A, f ,a>, where A is a set, f an operation on A
and a an element of A. Coercions are functions that are used
implicitly (they are inferred by the type checker) and allow, for
example, to use the structure A := <A, f, a> as
synonym for the carrier set A, as is often done in mathematical
practice. Apart from the inheritance and reuse of properties, the
algebraic hierarchy has proven very useful for reusing notations. [18 pp.]

F. Wiedijk, "Comparing mathematical provers." In: Andrea Asperti, Bruno Buchberger & James Davenport (eds.), Mathematical Knowledge Management, Proceedings of MKM 2003, Springer LNCS 2594, 188202, 2003: ps.gz pdf dvi tex
Abstract.
We compare fifteen systems for the formalizations of mathematics with the computer. We present several tables that list various properties of these programs. The three main dimensions on which we compare these systems are: the size of their library, the strength of their logic and their level of automation. [14 pp.]

F. Wiedijk, "A new implementation of Automath", Journal of Automated Reasoning 29, 365387, 2002: ps.gz pdf dvi tex
Abstract.
This paper presents aut, a modern Automath checker. It is a straightforward reimplementation of the Zandleven Automath checker from the seventies. It was implemented about five years ago, in the programming language C. It accepts both the AUT68 and AUTQE dialects of Automath. This program was written to restore a damaged version of Jutting's translation of Landau's Grundlagen. Some notable features:
 It is fast. On a 1GHz machine it will check the full Jutting formalization (736K of nonwhitespace Automath source) in 0.6 seconds.
 Its implementation of lambdaterms does not use named variables or de Bruijn indices (the two common approaches) but instead uses a graph representation. In this representation variables are represented by pointers to a binder.
 The program can compile an Automath text into one big "Automath single line" style lambdaterm. It outputs such a term using de Bruijn indices. (These lambdaterms cannot be checked by modern systems like Coq or Agda, because the lambdatyped lambdacalculi of de Bruijn are "incompatible" with the Pityped lambdacalculi of modern type theory.)
The source of aut is freely available on the Web. [25 pp.]

M. Wenzel & F. Wiedijk, "A comparison of the mathematical proof languages Mizar and Isar", Journal of Automated Reasoning 29, 389411, 2002: ps.gz pdf dvi tex
Abstract.
The mathematical proof checker Mizar by Andrzej Trybulec uses a proof input language that is much more readable than the input languages of most other proof assistants. This system also differs in many other respects from most current systems. John Harrison has shown that one can have a Mizar mode on top of a tactical prover, allowing one to combine a mathematical proof language with other styles of proof checking. Currently the only fully developed Mizar mode in this style is the Isar proof language for the Isabelle theorem prover. In fact the Isar language has become the official input language to the Isabelle system, even though many users still use its lowlevel tactical part only.
In this paper we compare Mizar and Isar. A small example, Euclid's proof of the existence of infinitely many primes, is shown in both systems. We also include slightly higherlevel views of formal proof sketches. Moreover a list of differences between Mizar and Isar is presented, highlighting the strengths of both systems from the perspective of endusers. Finally, we point out some key differences of the internal mechanisms of structured proof processing in either system. [26 pp.]

F. Wiedijk, "Formal proof sketches." In: Wan Fokkink & Jaco van de Pol (eds.), 7th Dutch Proof Tools Day, Program + Proceedings, CWI, Amsterdam, 2003: ps.gz pdf dvi tex
Abstract.
We define the notion of formal proof sketch for the mathematical language Mizar. We show by examples that formal proof sketches are very close to informal mathematical proofs. We discuss some ways in which formal proof sketches might be used to improve mathematical proof assistants. [19 pp.]

H. Geuvers & F. Wiedijk (eds.), Types for Proofs and Programs, International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 2428, 2002, Selected Papers, Springer LNCS 2646, viii+331 pp., 2003.

F. Wiedijk & J. Zwanenburg, "First Order Logic with Domain Conditions." In: David Basin & Burkhart Wolff (eds.), Theorem Proving in Higher Order Logics, Proceedings of TPHOLs 2003, Springer LNCS 2758, 221237, 2003: ps.gz pdf dvi tex
Abstract.
This paper addresses the crucial issue in the design of a proof development system of how to deal with partial functions and the related question of how to treat undefined terms. Often the problem is avoided by artificially making all functions total. However, that does not correspond to the practice of everyday mathematics.
In type theory partial functions are modeled by giving functions extra arguments which are proof objects. In that case it will not be possible to apply functions outside their domain. However, having proofs as first class objects has the disadvantage that it will be unfamiliar to most mathematicians. Also many proof tools (like the theorem prover Otter) will not be usable for such a logic. Finally expressions get difficult to read because of these proof objects.
The PVS system solves the problem of partial functions differently. PVS generates typecorrectness conditions (TCCs) for statements in its language. These are proof obligations that have to be satisfied "on the side" to show that statements are wellformed.
We propose a TCClike approach for the treatment of partial functions in type theory. We add domain conditions (DCs) to classical firstorder logic and show the equivalence with a first order system that treats partial functions in the style of type theory. [16 pp.]

F. Wiedijk, "Bewijzen nalopen met de computer, de QED utopie", Pythagoras, 43(3), 47, december 2003: ps.gz pdf dvi tex
No abstract.
[in Dutch, 3 pp.]

M. Giero & F. Wiedijk, "MMode, a Mizar Mode for the proof assistant Coq", report NIIIR0333, University of Nijmegen, 2003: ps.gz pdf dvi tex
Abstract.
We present a set of tactics for version 7.4 of the Coq proof assistant which makes it possible to write proofs for Coq in a language similar to the proof language of the Mizar system. These tactics can be used with any interface of Coq, and they can be freely mixed with the normal Coq tactics.
The system described in this report can be downloaded on the web. [55 pp.]

F. Wiedijk (ed.), Dutch Proof Tools Day 2004, Program + Proceedings, report NIIIR0429, University of Nijmegen, ii+81 pp., 2004: ps.gz pdf dvi

H. Geuvers & F. Wiedijk, "A logical framework with explicit conversions." In: Carsten Schürmann (ed.), LFM'04, Proceedings of the Fourth International Workshop on Logical Frameworks and MetaLanguages, Cork, Ireland, 3245, 2004: ps.gz pdf dvi tex
Abstract.
The type theory lambdaP corresponds to the logical framework LF. In this paper we present lambdaH, a variant of lambdaP where convertibility is not implemented by means of the customary conversion rule, but instead type conversions are made explicit in the terms. This means that the time to type check a lambdaH term is proportional to the size of the term itself.
We define an erasure} map from lambdaH to lambdaP, and show that through this map the type theory lambdaH corresponds exactly to lambdaP: any lambdaH judgment will be erased to a lambdaP judgment, and conversely each lambdaP judgment can be lifted to a lambdaH judgment.
We also show a version of subject reduction: if two lambdaH terms are provably convertible then their types are also provably convertible. [14 pp.]

L. CruzFilipe & F. Wiedijk, "Equational Reasoning in Algebraic Structures: a Complete Tactic", report NIIIR0431, University of Nijmegen, 2004: ps.gz pdf dvi tex
Abstract.
We present rational, a Coq tactic for equational reasoning in abelian groups, commutative rings, and fields. We give an mathematical description of the method that this tactic uses, which abstracts from Coq specifics.
We prove that the method that rational uses is correct, and that it is complete for groups and rings. Completeness means that the method succeeds in proving an equality if and only if that equality is provable from the the group/ring axioms. Finally we characterize in what way our method is incomplete for fields. [42 pp.]

F. Wiedijk, "Formal Proof Sketches." In: Stefano Berardi, Mario Coppo & Ferruccio Damiani (eds.), Types for Proofs and Programs: Third International Workshop, TYPES 2003, Torino, Italy, Springer LNCS 3085, 378393, 2004:
ps.gz pdf dvi tex
Abstract.
Formalized mathematics
currently does not look much like informal mathematics. Also, formalizing mathematics currently seems far too much work to be worth the time of the working mathematician. To address both of these problems we introduce the notion of a formal proof sketch. This is a proof representation that is in between a fully checkable formal proof and a statement without any proof at all. Although a formal proof sketch is too high level to be checkable by computer, it has a precise notion of correctness (hence the adjective formal).
We will show through examples that formal proof sketches can closely mimic already existing mathematical proofs. Therefore, although a formal proof sketch contains gaps in the reasoning from a formal point of view (which is why we call it a sketch), a mathematician probably would call such a text just a "proof". [16 pp.]

L. CruzFilipe & F. Wiedijk, "Hierarchical Reflection." In: Konrad Slind, Annette Bunker, Ganesh Gopalakrishnan (eds.), Theorem Proving in Higher Order Logics, Proceedings of TPHOLs 2004, Springer LNCS 3223, 6681, 2004: ps.gz pdf dvi tex
Abstract.
The technique of reflection is a way to automate proof construction in type theoretical proof assistants. Reflection is based on the definition of a type of syntactic expressions that gets interpreted in the domain of discourse. By allowing the interpretation function to be partial or even a relation one gets a more general method known as "partial reflection". In this paper we show how one can take advantage of the partiality of the interpretation to uniformly define a family of tactics for equational reasoning that will work in different algebraic structures. These tactics then follow the hierarchy of those algebraic structures in a natural way. [15 pp.]

L. CruzFilipe, H. Geuvers & F. Wiedijk, "CCoRN, the Constructive Coq Repository at Nijmegen." In: Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec (eds.), Mathematical Knowledge Management, Proceedings of MKM 2004, Springer LNCS 3119, 88103, 2004: ps.gz pdf dvi tex
Abstract.
We present CCoRN, the Constructive Coq Repository at Nijmegen. It consists of a library of constructive algebra and analysis, formalized in the theorem prover Coq. In this paper we explain the structure, the contents and the use of the library. Moreover we discuss the motivation and the (possible) applications of such a library. [16 pp.]

M. Beeson & F. Wiedijk, "The meaning of infinity in calculus and computer algebra Systems." Journal of Symbolic Computation 39, 523538, 2005: ps.gz pdf dvi tex
Abstract.
We use filters of open sets to provide a semantics justifying the use of infinity in informal limit calculations in calculus, and in the same kind of calculations in computer algebra. We compare the behavior of these filters to the way Mathematica behaves when calculating with infinity.
A proper semantics for computer algebra expressions is necessary not only for the correct application of those methods, but also in order to use results and methods from computer algebra in theorem provers. The computer algebra method under discussion in this paper is the use of rewrite rules to evaluate limits involving infinity.
Unlike in other areas of computer algebra, where the problem has been a mismatch between a known semantics and implementations, we here provide the first precise semantics.
[17 pp.]

H. Barendregt & F. Wiedijk, "The Challenge of Computer Mathematics", Transactions A of the Royal Society 363 no. 1835, 23512375, 2005: ps.gz pdf dvi tex
Abstract.
Progress in the foundations of mathematics has
made it possible to formulate all thinkable mathematical concepts,
algorithms and proofs in one language and in an impeccable way. This is
not in spite of, but partially based on the famous results of Gödel
and Turing. In this way statements are about mathematical objects
and algorithms, proofs show the correctness of statements
and computations, and computations are dealing with objects
and proofs. Interactive computer systems for a full integration
of defining, computing and proving are based on this. The human
defines concepts, constructs algorithms and provides proofs, while the
machine checks that the definitions are wellformed and the proofs and
computations are correct. Results formalised so far demonstrate the
feasibility of this "Computer Mathematics". Also there are very good
applications. The challenge is to make the systems more
mathematicianfriendly, by building libraries and tools. The eventual
goal is to help humans to learn, develop, communicate, referee and
apply mathematics.
[23 pp.]

H. Barendregt & F. Wiedijk, "Bewijzen: romantisch of cool", Euclides, 2006: ps.gz pdf dvi tex
Abstract.
Computers kunnen ons helpen wiskunde te doen
door voor ons te rekenen, met getallen of symbolisch. Systemen
hiervoor zijn goed ontwikkeld. Er worden nu ook computersystemen
ontwikkeld, de zogenaamde wiskundige assistenten, die ons zelfs kunnen
helpen met het verifiëren en verder ontwikkelen van het vak. Het
menselijke vernuft zal hierdoor niet overbodig worden.
[in Dutch, 10 pp.]

F. Wiedijk, "On the usefulness of formal methods", Nieuwsbrief van de NVTI, 1423, 2006: ps.gz pdf dvi tex
No abstract.
[10 pp.]

F. Wiedijk (ed.), The Seventeen Provers of the World, foreword by Dana S. Scott, Springer LNAI 3600, 2006.
Abstract.
We compare the styles of several proof assistants for mathematics. We present Pythagoras' proof of the irrationality of sqrt(2) both informal and formalized in (1) HOL, (2) Mizar, (3) PVS, (4) Coq, (5) Otter/Ivy, (6) Isabelle/Isar, (7) Alfa/Agda, (8) ACL2, (9) PhoX, (10) IMPS, (11) Metamath, (12) Theorema, (13) Lego, (14) Nuprl, (15) Omega, (16) B method, (17) Minlog. [169 pp.]

F. Wiedijk, "Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics", Journal of Applied Logic 4, 622645, 2006: ps.gz pdf dvi tex
Abstract.
This paper presents Automath encodings (which also are valid in LF/lambdaP) of various kinds of foundations of mathematics. Then it compares these encodings according to their size, to find out which foundation is the simplest.
The systems analyzed in this way are two kinds of set theory (ZFC and NF), two systems based on Church's higher order logic (Isabelle/Pure and HOL), three kinds of type theory (the calculus of constructions, Luo's extended calculus of constructions, and MartinLöf predicative type theory) and one foundation based on category theory.
The conclusions of this paper are that the simplest system is type theory (the calculus of constructions) but that type theories that know about serious mathematics are not simple at all. Set theory is one of the simpler systems too. Higher order logic is the simplest if one looks at the number of concepts (twentyfive) needed to explain the system. On the other side of the scale, category theory is relatively complex, as is MartinLöf's type theory. [19 pp.]

H. Geuvers, M. Niqui, B. Spitters & F. Wiedijk, "Constructive analysis, types and exact real numbers." In: B. Spitters, H. Geuvers, M. Niqui & F. Wiedijk (eds.), special issue "Constructive analysis, types and exact real numbers", Mathematical Structures in Computer Science 17(1), 336, 2007: ps.gz pdf dvi tex
Abstract.
In the present paper, we will discuss various aspects of
computable/constructive analysis, namely semantics, proofs and
computations. We will present some of the problems and solutions of
exact real arithmetic varying from concrete implementations,
representation and algorithms to various models for real
computation. We then put these models in a uniform framework using
realisability, opening the door for the use of type theoretic and
coalgebraic constructions both in computing and reasoning about
these computations. We will indicate that it is often natural to use
constructive logic to reason about these computations.
[36 pp.]

C. Kaliszyk & F. Wiedijk, "Certified Computer Algebra on top of an Interactive Theorem Prover." In: M. Kauers, M. Kerber, R. Miner & W. Windsteiger (eds.), Towards Mechanized Mathematical Assistants, Calculemus 2007, Hagenberg, LNAI 4573, 94105, 2007: ps.gz pdf dvi tex
Abstract.
We present a prototype of a computer algebra system that is built on top of
a proof assistant, HOL Light. This architecture
guarantees that one can be certain that the system will make no
mistakes. All expressions in the system will have precise semantics, and
the proof assistant will check the correctness of all simplifications
according to this semantics. The system actually proves each
simplification performed by the computer algebra system.
Although our system is built on top of a proof assistant, we designed the
user interface to be very close in spirit to the interface of systems like
Maple and Mathematica. The system, therefore, allows the user
to easily probe the underlying automation of the proof assistant for
strengths and weaknesses with respect to the automation of mainstream
computer algebra systems. The system that we present is a
prototype, but can be straightforwardly scaled up to a practical computer
algebra system.
[13 pp.]

F. Wiedijk, "The QED Manifesto Revisited." In: R. Matuszwski & A. Zalewska (eds.), From Insight to Proof, Festschrift in Honour of Andrzej Trybulec, 121133, 2007: ps.gz pdf dvi tex
Abstract.
We present an overview of the current state of formalization of
mathematics, and argue what will be needed to make the vision
from the QED manifesto come true.
[14 pp.]

J. Carette & F. Wiedijk (eds.), Programming Languages for Mechanized Mathematics Workshop, Informal Proceedings, RISCLinz Report Series No. 0710, 90 pp., 2007.
No abstract.

C. Kaliszyk, F. Wiedijk, M. Hendriks & F. van Raamsdonk, "Teaching logic using a stateoftheart proof assistant." In: H. Geuvers & P. Courtieu (eds.), PATE'07, International Workshop on Proof Assistants and Types in Education, 3750, 2007: ps.gz pdf tex
Abstract.
This article describes the system ProofWeb
that is currently being developed in Nijmegen
and Amsterdam for
teaching logic to undergraduate computer science students.
This system is based on the higher order proof assistant Coq,
and is made available to the students through an interactive web interface.
Part of this system will be a large database of logic problems.
This database will also hold the solutions of the students.
This means that the students do not need to install anything to be able
to use the system (not even a browser plugin), and that the teachers
will be able to centrally track progress of the students.
The system makes the full power of Coq available to the students,
but simultaneously presents the logic problems in a way that
is customary in undergraduate logic courses.
Both styles of presenting natural deduction proofs (Gentzenstyle "tree view"
and Fitchstyle "box view") are supported.
Part of the system is a parser that indicates whether the students
used the automation of Coq to solve their problems or that they
solved it themselves using only the inference rules of the logic.
For these inference rules dedicated tactics for Coq have been developed.
The system has already been used in a type theory
course, and is currently being further developed in the first year logic course
of computer science in Nijmegen.
[15 pp.]

F. Wiedijk, "Mizar's Soft Type System." In: K. Schneider & J. Brandt (eds.), Theorem Proving in Higher Order Logics 2007, LNCS 4732, 383399, 2007: ps.gz pdf dvi tex
Abstract.
In Mizar, unlike in most other proof assistants,
the types are not part of the foundations of the
system.
Mizar is based on untyped set theory, which means
that in Mizar expressions are typed but the values of
those expressions are not.
In this paper we present the Mizar type system
as a collection of type inference rules.
We will interpret Mizar types as soft types,
by translating Mizar's type judgments into sequents of
untyped
first order predicate logic.
We will then prove that the Mizar type system is
correct with respect to this translation
in the sense that each derivable type judgment translates
to a provable sequent.
[17 pp.]

S. Autexier, J. Campbell, J. Rubio, V. Sorge, Masakazu Suzuki & F. Wiedijk (eds.), Intelligent Computer Mathematics, 9th International Conference, AISC 2008, 15th Symposium, Calculemus 2008, 7th International Conference, MKM 2008, Birmingham, UK, July 28August 1, 2008, Proceedings, Springer LNCS 5144, xiv+600 pp., 2008.

F. Wiedijk, "De kunst van het bewijzen." In: Wiskunde en profil, Het gezicht van de wiskunde, Vakantiecursus 2008, CWI syllabus 58, 107130, 2008: ps.gz pdf dvi tex
Abstract: ps.gz pdf dvi tex
[23 pp.]

C. Kaliszyk, F. van Raamsdonk, F. Wiedijk, H. Wupper, M. Hendriks & R. de Vrijer, "Deduction using the ProofWeb system", report ICISR08016, Radboud University Nijmegen, 2008: ps.gz pdf dvi tex
Abstract.
This is the manual of the ProofWeb system that was
implemented at the Radboud University Nijmegen and the Free University Amsterdam
in the SURF education innovation project Web deduction for education in formal thinking.
[54 pp.]

P. Corbineau, H. Geuvers, C. Kaliszyk, J. McKinna & F. Wiedijk, "Position paper: A real Semantic Web for mathematics deserves a real semantics", In: C. Lange, S. Schaffer, H. SkafMolli & M. Völkel (eds.), Proceedings of the 3rd Semantic Wiki Workshop (SemWiki 2008) at the 5th European Semantic Web Conference (ESWC 2008), 2008: ps.gz pdf dvi tex
Abstract.
Mathematical documents, and their instrumentation by computers, have
rich structure at the layers of presentation, metadata and semantics,
as objects in a system for formal mathematical logic. Semantic Web
tools support the first two of these, with little, if any,
contribution to the third, while Proof Assistants instrument
the third layer, typically with bespoke approaches to the first two.
Our position is that a web of mathematical documents, definitions
and proofs should be given a fullyfledged semantics in terms of the
third layer. We propose a "MathWiki" to harness
Web 2.0 tools and techniques to the rich semantics
furnished by contemporary Proof Assistants.
[5 pp.]

F. Wiedijk, "Formal proof  getting started", Notices of the AMS 55(11), 14081414, 2008: ps.gz pdf dvi tex
No abstract.
[13 pp.]

F. Wiedijk, "Formalizing Arrow's theorem", Sadhana 34(1), 193220, 2009: ps.gz pdf dvi tex
Abstract.
We present a small project in which we encoded a proof of Arrow's theorem 
probably the most famous results in the economics field of social
choice theory  in the computer using the Mizar system.
We both discuss the details of this specific project, as well as describe the
process of formalization (encoding proofs in the computer)
in general.
[32 pp.]

F. Wiedijk, "Practising logic through the web", Nieuwsbrief van de NVTI, 13, 6168, 2009: ps.gz pdf dvi tex
Abstract.
We present the ProofWeb system for practising natural deduction in predicate logic and for remotely working with the Coq proof assistant. The ProofWeb system can be used for free, both for trying it out as a guest as well as for hosting computer labs for logic and proof assistant courses, on the Nijmegen ProofWeb server http://proofweb.cs.ru.nl/.
[8 pp.]

G. Cornelissen, W. de Graaf, W. van der Kallen, J. Sijsling, B. de Smit, J. Stevens & F. Wiedijk, "Wiskundig onderzoek per computer?", Nieuw Archief voor Wiskunde 5/10, nr. 3, 197200, 2009: ps.gz pdf dvi tex
No abstract.
[1 p.]

M. Niqui & F. Wiedijk, "`Many Digits' Friendly Competition", report ICISR09007, University of Nijmegen, 2009: ps.gz pdf dvi tex
Abstract.
In this article we give an account of the "Many Digits" friendly competition,
a competition between arbitrary precision arithmetic packages that was
organised following Jens Blanck, Exact Real Arithmetic Systems: Results of Competition, and was held on October 34, 2005 in
order to investigate the state of the art in the field of exact and arbitrary
precision arithmetic.
The competition consisted of two types of problems, a basic and an
intermediate set. The basic problems consisted of simple expressions
involving elementary functions. The intermediate problems involved more
mathematical construct or slightly more programming. A solution consisted of a sequence of decimal digits, for most problems 10000 digits. The systems were
required to calculate the solution within two minutes and depending on their
success retry the problem with a higher/lower number of digits. The
competition had nine participants, some of them competing remotely.
[122 pp.]

F. Wiedijk, "Statistics on digital libraries of mathematics". In: Studies in Logic Grammar and Rhetoric 18(31), Computer Reconstruction of the Body of Mathematics, 2009: ps.gz pdf dvi tex
Abstract.
We present statistics on the standard
libraries of four major proof assistants for mathematics:
HOL Light, Isabelle/HOL, Coq and Mizar. [15 pp.]

C. Tankink, H. Geuvers, J. McKinna & F. Wiedijk, "Proviola: a Tool for Proof Reanimation". In: S. Autexier, J. Calmet, D. Delahaye, P.D.F. Ion, L. Rideau, R. Rioboo & A.P. Sexton (eds.), Intelligent Computer Mathematics, 10th International Conference, AISC 2010, 17th Symposium, Calculemus 2010 and 9th International Conference, MKM 2010, Springer LNAI 6167, 440454, 2010: ps.gz pdf
Abstract.
To improve on existing models of interaction with a proof
assistant (PA), in particular for storage and replay of proofs, we introduce
three related concepts, those of: a proof movie, consisting of
frames which record both user input and the corresponding PA response;
a camera, which films a user's interactive session with a PA as a movie;
and a proviola, which replays a movie framebyframe to a third party.
In this paper we describe the movie data structure and we discuss a prototype
implementation of the camera and proviola based on the ProofWeb
system. ProofWeb uncouples the interaction with a PA via a web
interface (the client) from the actual PA that resides on the server. Our
camera films a movie by "listening" to the ProofWeb communication.
The first reason for developing movies is to uncouple the reviewing of a
formal proof from the PA used to develop it: the movie concept enables
users to discuss small code fragments without the need to install the PA
or to load a whole library into it.
Other advantages include the possibility to develop a separate commentary
track to discuss or explain the PA interaction. We assert that
a combined camera+proviola provides a generic layer between a client
(user) and a server (PA). Finally we claim that movies are the right
type of data to be stored in an encyclopedia of formalized mathematics,
based on our experience in filming the Coq standard library.
[15 pp.]

H. Geuvers, R. Krebbers, J. McKinna & F. Wiedijk, "Pure Type Systems without Explicit Contexts". In: K. Crary & M. Miculan (eds.), Proceedings of the 5th International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, EPTCS 34, 5367, 2010: ps.gz pdf dvi tex
Abstract.
We present an approach to type theory in which the typing judgments do not have explicit contexts.
Instead of judgments of shape Γ  A : B, our systems just have judgments of shape A : B. A key
feature is that we distinguish free and bound variables even in pseudoterms.
Specifically we give the rules of the "Pure Type System" class of type theories in this style. We
prove that the typing judgments of these systems correspond in a natural way with those of Pure
Type Systems as traditionally formulated. I.e., our systems have exactly the same welltyped terms
as traditional presentations of type theory.
Our system can be seen as a type theory in which all type judgments share an identical, infinite,
typing context that has infinitely many variables for each possible type. For this reason we call our
system . This name means to suggest that our type judgment A : B should be read as Γ_{∞}  A : B,
with a fixed infinite type context called Γ_{∞}.
[15 pp.]

F. Wiedijk, "Stateless HOL". In: T. Hirschowitz (ed.), Types for Proofs and Programs, TYPES 2009, Revised Selected Papers, EPTCS 53, 4761, 2011: ps.gz pdf dvi tex
Abstract.
We present a version of the HOL Light system that supports
undoing definitions in such a way that this does not
compromise the soundness of the logic. In our system
the code that keeps track of the constants that have
been defined thus far has been moved out of the kernel.
This means that the kernel now is purely functional.
The changes to the system are small. All existing HOL Light
developments can be run by the stateless system with only
minor changes.
The basic principle behind the system is not to name
constants by strings, but by pairs consisting of a string
and a definition. This means that the data structures
for the terms are all merged into one big graph. OCaml 
the implementation language of the system  can use pointer
equality to establish equality of data structures fast.
This allows the system to run at acceptable speeds.
Our system runs at about 85% of the speed of the stateful
version of HOL Light.
[15 pp.]

R. Krebbers & F. Wiedijk, A formalization of the C99 standard in HOL, isabelle and Coq. In: J.H. Davenport, W.M. Farmer, F. Rabe, & J. Urban (eds.), Intelligent Computer Mathematics, Calculemus 2011 and MKM 2011, LNAI 6824, 301303, 2011: ps.gz pdf dvi tex
Abstract.
We recently started the Formalin project to create a formal version of the C99 standard for the C programming language. We are writing three matching formalizations for the interactive theorem provers HOL4, Isabelle/HOL and Coq, that all closely follow the existing C99 standard text. The project runs from 2011 to 2015, and involves a full time PhD student, a half time researcher and several scientific advisors. The project differs from existing work in that our aim is to formalize the full C99 standard. This means that we treat the C preprocessor, the C standard library, floating point arithmetic, and "dirty" C features like signal handling and volatile variables. Importantly, this means we also treat embedded C programs without explicit input/output.
[3 pp.]

M. van Eekelen, H. Geuvers, J. Schmalz & F. Wiedijk (eds.), Interactive Theorem Proving, Proceedings of the Second International Conference on Interactive Theorem Proving, ITP 2011, Berg en Dal. The Netherlands, Springer LNCS 6898. 382 pp., 2011.

F. Wiedijk, "Pollackinconsistency". In: C. Sacerdoti Coen & D. Aspinall, UITP 2010, 9th International Workshop on User Interfaces for Theorem Provers, ENTCS 285, 85100, 2012: ps.gz pdf dvi tex
Abstract.
We present an approach to type theory in which the typing judgments do not have explicit contexts.
Instead of judgments of shape Γ  A : B, our systems just have judgments of shape A : B. A key
feature is that we distinguish free and bound variables even in pseudoterms.
Specifically we give the rules of the "Pure Type System" class of type theories in this style. We
prove that the typing judgments of these systems correspond in a natural way with those of Pure
Type Systems as traditionally formulated. I.e., our systems have exactly the same welltyped terms
as traditional presentations of type theory.
Our system can be seen as a type theory in which all type judgments share an identical, infinite,
typing context that has infinitely many variables for each possible type. For this reason we call our
system . This name means to suggest that our type judgment A : B should be read as Γ_{∞}  A : B,
with a fixed infinite type context called Γ_{∞}.
[15 pp.]

F. Wiedijk, A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving. Logical Methods in Computer Science 8(1), 126, 2012: ps.gz pdf dvi tex
Abstract.
We propose a synthesis of the two proof styles of interactive
theorem proving: the procedural style (where proofs are
scripts of commands, like in Coq) and the declarative style
(where proofs are texts in a controlled natural language,
like in Isabelle/Isar). Our approach combines the advantages
of the declarative style  the possibility to write formal
proofs like normal mathematical text  and the procedural
style  strong automation and help with shaping the proofs,
including determining the statements of intermediate steps.
Our approach is new, and differs significantly from the ways
in which the procedural and declarative proof styles have
been combined before in the Isabelle, Ssreflect and Matita systems.
Our approach is generic and can be implemented on top of
any procedural interactive theorem prover, regardless of
its architecture and logical foundations.
To show the viability of our proposed approach, we fully
implemented it as a proof interface called miz3, on top of
the HOL Light interactive theorem prover. The declarative
language that this interface uses is a slight variant
of the language of the Mizar system, and can be used for
any interactive theorem prover regardless of its logical
foundations. The miz3 interface allows easy access to
the full set of tactics and formal libraries of HOL Light,
and as such has `industrial strength'.
Our approach gives a way to automatically convert any
procedural proof to a declarative counterpart, where
the converted proof is similar in size to the original.
As all declarative systems have essentially the same proof
language, this gives a straightforward way to port proofs
between interactive theorem provers.
[26 pp.]

F. Wiedijk, "Handbook of Practical Logic and Automated Reasoning," by John R. Harrison, Cambridge University Press, 2009. Journal of Automated Reasoning 49(1), 107109, 2012: ps.gz pdf dvi tex
No abstract.
[3 pp.]

R. Krebbers & F. Wiedijk, Separation Logic for Nonlocal Control Flow and Block Scope Variables. In: F. Pfenning (ed.), Foundations of Software Science and Computation Structures  16th International Conference, FOSSACS 2013, LNCS 7794, 257272, 2013: ps.gz pdf dvi tex
Abstract.
We present an approach for handling nonlocal control flow (goto and return
statements) in the presence of allocation and deallocation of block scope
variables in imperative programming languages.
We define a small step operational semantics and an axiomatic
semantics (in the form of a separation logic) for a small Clike language
that combines these two features,
and which also supports pointers to block scope variables.
Our operational semantics represents the program state through a
generalization of Huet's zipper data structure.
We prove soundness of our axiomatic semantics with respect to our
operational semantics.
This proof has been fully formalized in Coq.
[16 pp.]
publications
notes
mizar
talks
(last modification 20130409)
