1. "The De Bruijn Factor": ps.gz pdf dvi tex

   Abstract. 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.]

2. "Selecting the Domain of a Standard Library for a Mathematical Proof Checker": ps.gz pdf dvi tex

   Abstract. 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.]

3. "Estimating the Cost of a Standard Library for a Mathematical Proof Checker": ps.gz pdf dvi tex

   Abstract. 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.]

4. "Conditional Computing": ps.gz pdf dvi tex

   Abstract. 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.]

5. "Formalizing Elementary Analysis Rigorously": ps.gz pdf dvi tex

   Abstract. 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]

6. "Web-deductie voor het onderwijs in formeel denken": ps.gz pdf doc

   No abstract. [in Dutch, 7 pp.]

7. "Proof Checking the Proof Checker": ps.gz pdf dvi tex

   Abstract. 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 fully correct. 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. [16 pp.]
   [rejected PhD project proposal for the NWO free competition 2009]

8. "Mizar: An Impression": ps.gz pdf dvi tex

   Abstract. 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.]

9. "Writing a Mizar article in nine easy steps": ps.gz pdf dvi tex

   No abstract. [54 pp.]

10. "CHECKER": ps.gz pdf dvi tex

    Abstract. 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.]

11. "A proposed syntax for binders in Mizar": ps.gz pdf dvi tex

    Abstract. 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.]

12. "The Mathematical Vernacular": ps.gz pdf dvi tex

    Abstract. 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.]

13. "The formal proof sketch challenge": ps.gz pdf dvi tex

    Abstract. 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.]

14. "Ten Formal Proof Sketches": ps.gz pdf dvi tex

    Abstract. This note collects the formal proof sketches that I have done. [26 pp.]

15. "The mu-inverse for the HOL Light reals": ps.gz pdf dvi tex

    Abstract. We present an alternative definition of the multiplicative inverse for the real numbers as formalized in John Harrison's HOL Light system. [5 pp.]

16. "Encoding the HOL Light logic in Coq": ps.gz pdf dvi tex

    Abstract. 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.]

17. "Subtleties of the ISO C standard", with Robbert Krebbers: ps.gz pdf dvi tex

    Abstract. n our efforts 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. Furthermore, we discuss why the C standard should address the possibility of stack overflow, and we argue that evaluation of C expressions does not preserve typing in the presence of variable length array types. [10 pp.]

(last modification 2014-10-27)