"The De Bruijn Factor": ps.gz pdf dvi tex
We study de Bruijn's "loss factor" between the size of an ordinary mathematical exposition and its full formal translation inside a computer. This factor is determined by a combination of the amount of detail present in the original text and the expressivity of the system used to do the formalization. For three specific examples this factor turns out to be approximately equal to four. [5 pp.]
"Selecting the Domain of a Standard Library for a Mathematical Proof Checker": ps.gz pdf dvi tex
By investigating the programs of the mathematics studies in the six main Dutch universities, we determine the basic subject areas that should be present in a standard library for a mathematical proof checker. An approach to realize such a library is outlined. [5 pp.]
"Estimating the Cost of a Standard Library for a Mathematical Proof Checker": ps.gz pdf dvi tex
We estimate the cost of formalizing a proper standard library for proof checking of mathematics in the spirit of the QED project. Apparently it will take approximately 140 man-years. This estimate does not include the development of the proof checking program, nor does it include work on the metatheory of that program.
This should discourage any individual or small research group to think they can reach anything like the goal of the QED project on their own. [6 pp.]
"Conditional Computing": ps.gz pdf dvi tex
We show that current computer algebra systems are not suitable for use in proof checking, because they don't answer the right kind of question. By analyzing the calculations from a sample formalization, we find that calculations as they occur in proof checking make use of results of previous calculations (conditions). We list a number of such conditional calculation problems and argue that because of these conditions, current computer algebra packages like Maple and Mathematica are not able to solve them. [8 pp.]
"Formalizing Elementary Analysis Rigorously": ps.gz pdf dvi tex
Two classes of systems exist for working with mathematical formulas on a computer: "computer algebra" programs (of which Mathematica is the best known) and "proof assistants" (programs for the verification of mathematical proofs). The first kind of system (computer algebra) manipulates formulas that do not necessarily have a precise mathematical meaning (those formulas do not have a "semantics"). The second kind of system (proof assistants) manipulates formulas that do have a precise meaning, but those often do not much resemble the formulas that one encounters in mathematical textbooks.
The F.E.A.R. project will design a language of formulas that have a precise semantics, but still resemble the traditional formulas found in textbooks. We will do this by translating a section from a classic handbook of mathematical formulas (the Handbook of Mathematical Functions by Abramowitz & Stegun) into a proof assistant. Since the formulas will be entered in a proof assistant, a sound semantics is guaranteed. Also it will be easy to judge whether the translation sufficiently resembles theoriginal formulas from the handbook. [14 pp.]
[accepted PhD project proposal for the NWO open competition 2004]
"Web-deductie voor het onderwijs in formeel denken": ps.gz pdf doc
[in Dutch, 7 pp.]
"Proof Checking the Proof Checker": ps.gz pdf dvi tex
It is considered a fact of life that all serious
computer programs contain errors, so-called "bugs".
Empirical data indicates that production software has around
two bugs per thousand lines of source code,
and even programs used on space missions by NASA are believed to have around
0.1 bugs per thousand lines of code.
Interactive theorem proving is
a technology for building programs
that almost certainly have zero bugs per thousand lines of code.
Already some significant programs have been shown to be
For instance both the certified C compiler
of Xavier Leroy and the programs from the proof of
the Four Color Theorem by Georges Gonthier
have been formally shown -- with a fully computer-checked
proof -- to do
precisely what they should do,
and therefore are guaranteed to be bug-free.
This technology of interactive theorem proving for software correctness
is on the verge of becoming widely applicable.
A sign that this moment has not yet arrived
is that currently it is not even used by the
very people who build tools for it.
Thus far, no system for interactive theorem proving
has been formally proved bug-free.
The Proof Checking the Proof Checker project
will change this situation.
At the end of this project
one of the best systems for
interactive theorem proving will have used its own technology to establish
that it is completely sound.
Furthermore not just a model, but the actual source code of the program
will have been proved correct.
[rejected PhD project proposal for the NWO free competition 2009]
"Mizar: An Impression": ps.gz pdf dvi tex
This note presents an introduction to the Mizar system, followed by a brief comparison between Mizar and Coq. Appended are a Mizar grammar and an annotated example of a complete Mizar article. [42 pp.]
"Writing a Mizar article in nine easy steps": ps.gz pdf dvi tex
"CHECKER": ps.gz pdf dvi tex
This is a compilation of a series of e-mail messages sent to me by Andrzej Trybulec. The basic inference step (by) of the Mizar system is described. [11 pp.]
"A proposed syntax for binders in Mizar": ps.gz pdf dvi tex
Binders like "lim" (for limits), "Sigma" (for summation) and "integral" (for integration) are an essential part of the language of mathematics. They are the "higher order" elements of mathematical expressions.
At the TYPES meeting of 2003 in Turin, Andrzej Trybulec told me that the reason that Mizar did not have binders was that nobody had proposed a good syntax for them yet. To take this reason away, we will present a syntax for binders in Mizar. [7 pp.]
"The Mathematical Vernacular": ps.gz pdf dvi tex
A "mathematical vernacular" is a formal language for writing mathematical proofs which resembles the natural language from mathematical texts. A number of systems (Hyperproof, Mizar, Isabelle/Isar) all basically have the same proof language. It consists of the combination of natural deduction with first order inference steps. In this note we compare these three languages and present a simplified common version. [9 pp.]
"The formal proof sketch challenge": ps.gz pdf dvi tex
A formal proof sketch is a way to present a formal proof in a style that is close to an informal proof, but which also is a skeleton of the full formal proof (this makes it easy to relate the presentation to the detailed formalization.) Recently to us every informal proof has started to feel like a challenge, to write down the corresponding formal proof sketch. We take on this challenge for the informal proof of Newman's lemma from Henk Barendregt's book about lambda-calculus. The specific difficulty of that proof is its main part, which just is a pair of diagrams without any explanation. [15 pp.]
"Nine Formal Proof Sketches": ps.gz pdf dvi tex
This note collects the formal proof sketches that I have done. [26 pp.]
"The mu-inverse for the HOL Light reals": ps.gz pdf dvi tex
We present an alternative definition of the multiplicative inverse for the real numbers as formalized in John Harrison's HOL Light system. [5 pp.]
"Encoding the HOL Light logic in Coq": ps.gz pdf dvi tex
We show how to encode the HOL Light logic in Coq. This makes an automatic translation of HOL proofs to Coq possible. The translated HOL proofs refer to translated HOL data types but those data types can be related to the standard Coq data types, making the HOL results useful for Coq. The translated proofs have a size linear in the time HOL takes to process the original proofs. However the constant of linearity is large. The approach described in this paper is similar to the method of Pavel Naumov, Mark-Oliver Stehr and José Mesequer for translating HOL98 proofs to Nuprl. [21 pp.]
"Subtleties of the ISO C standard", with Robbert Krebbers: ps.gz pdf dvi tex
to formalize C11 (the ISO
standard of the C programming language) we discovered many unexpected
subtleties that make formalization of that standard difficult.
Most of these difficulties are the result of the C standard giving
compilers room for strong optimizations based on aliasing analysis.
We discuss some of these subtleties and indicate how they may be addressed in
a formal C semantics.
we discuss why the C standard should address the possibility
of stack overflow,
we argue that evaluation of C expressions does not
preserve typing in the presence of variable length array types. [10 pp.]