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

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

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

  4. 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, 341-361, 1991.

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

  6. 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, 162-178, 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.]

  7. 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, 378-393, 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.]

  8. 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, 96-111, 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.]

  9. 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, 271-286, 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 dependent-typed 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.]

  10. F. Wiedijk, "Comparing mathematical provers." In: Andrea Asperti, Bruno Buchberger & James Davenport (eds.), Mathematical Knowledge Management, Proceedings of MKM 2003, Springer LNCS 2594, 188-202, 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.]

  11. F. Wiedijk, "A new implementation of Automath", Journal of Automated Reasoning 29, 365-387, 2002: ps.gz pdf dvi tex

    Abstract. This paper presents aut, a modern Automath checker. It is a straight-forward re-implementation of the Zandleven Automath checker from the seventies. It was implemented about five years ago, in the programming language C. It accepts both the AUT-68 and AUT-QE 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 non-whitespace Automath source) in 0.6 seconds.
    - Its implementation of lambda-terms 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 lambda-term. It outputs such a term using de Bruijn indices. (These lambda-terms cannot be checked by modern systems like Coq or Agda, because the lambda-typed lambda-calculi of de Bruijn are "incompatible" with the Pi-typed lambda-calculi of modern type theory.)
    The source of aut is freely available on the Web. [25 pp.]

  12. M. Wenzel & F. Wiedijk, "A comparison of the mathematical proof languages Mizar and Isar", Journal of Automated Reasoning 29, 389-411, 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 low-level 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 higher-level 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 end-users. Finally, we point out some key differences of the internal mechanisms of structured proof processing in either system. [26 pp.]

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

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

  15. 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, 221-237, 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 type-correctness conditions (TCCs) for statements in its language. These are proof obligations that have to be satisfied "on the side" to show that statements are well-formed.
    We propose a TCC-like approach for the treatment of partial functions in type theory. We add domain conditions (DCs) to classical first-order logic and show the equivalence with a first order system that treats partial functions in the style of type theory. [16 pp.]

  16. F. Wiedijk, "Bewijzen nalopen met de computer, de QED utopie", Pythagoras, 43(3), 4-7, december 2003: ps.gz pdf dvi tex

    No abstract. [in Dutch, 3 pp.]

  17. M. Giero & F. Wiedijk, "MMode, a Mizar Mode for the proof assistant Coq", report NIII-R0333, 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.]

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

  19. 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 Meta-Languages, Cork, Ireland, 32-45, 2004: ps.gz pdf dvi tex

    Abstract. The type theory lambda-P corresponds to the logical framework LF. In this paper we present lambda-H, a variant of lambda-P 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 lambda-H term is proportional to the size of the term itself.
    We define an erasure} map from lambda-H to lambda-P, and show that through this map the type theory lambda-H corresponds exactly to lambda-P: any lambda-H judgment will be erased to a lambda-P judgment, and conversely each lambda-P judgment can be lifted to a lambda-H judgment.
    We also show a version of subject reduction: if two lambda-H terms are provably convertible then their types are also provably convertible. [14 pp.]

  20. L. Cruz-Filipe & F. Wiedijk, "Equational Reasoning in Algebraic Structures: a Complete Tactic", report NIII-R0431, 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.]

  21. 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, 378-393, 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.]

  22. L. Cruz-Filipe & 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, 66-81, 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.]

  23. L. Cruz-Filipe, H. Geuvers & F. Wiedijk, "C-CoRN, the Constructive Coq Repository at Nijmegen." In: Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec (eds.), Mathematical Knowledge Management, Proceedings of MKM 2004, Springer LNCS 3119, 88-103, 2004: ps.gz pdf dvi tex

    Abstract. We present C-CoRN, 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.]

  24. M. Beeson & F. Wiedijk, "The meaning of infinity in calculus and computer algebra Systems." Journal of Symbolic Computation 39, 523-538, 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.]

  25. H. Barendregt & F. Wiedijk, "The Challenge of Computer Mathematics", Transactions A of the Royal Society 363 no. 1835, 2351-2375, 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 well-formed 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 mathematician-friendly, by building libraries and tools. The eventual goal is to help humans to learn, develop, communicate, referee and apply mathematics. [23 pp.]

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

  27. F. Wiedijk, "On the usefulness of formal methods", Nieuwsbrief van de NVTI, 14-23, 2006: ps.gz pdf dvi tex

    No abstract. [10 pp.]

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

  29. F. Wiedijk, "Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics", Journal of Applied Logic 4, 622-645, 2006: ps.gz pdf dvi tex

    Abstract. This paper presents Automath encodings (which also are valid in LF/lambda-P) 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 Martin-Lö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 (twenty-five) needed to explain the system. On the other side of the scale, category theory is relatively complex, as is Martin-Löf's type theory. [19 pp.]

  30. 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), 3-36, 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.]

  31. 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, 94-105, 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.]

  32. F. Wiedijk, "The QED Manifesto Revisited." In: R. Matuszwski & A. Zalewska (eds.), From Insight to Proof, Festschrift in Honour of Andrzej Trybulec, 121-133, 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.]

  33. J. Carette & F. Wiedijk (eds.), Programming Languages for Mechanized Mathematics Workshop, Informal Proceedings, RISC-Linz Report Series No. 07-10, 90 pp., 2007.

    No abstract.

  34. C. Kaliszyk, F. Wiedijk, M. Hendriks & F. van Raamsdonk, "Teaching logic using a state-of-the-art proof assistant." In: H. Geuvers & P. Courtieu (eds.), PATE'07, International Workshop on Proof Assistants and Types in Education, 37-50, 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 plug-in), 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 (Gentzen-style "tree view" and Fitch-style "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.]

  35. F. Wiedijk, "Mizar's Soft Type System." In: K. Schneider & J. Brandt (eds.), Theorem Proving in Higher Order Logics 2007, LNCS 4732, 383-399, 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.]

  36. 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 28-August 1, 2008, Proceedings, Springer LNCS 5144, xiv+600 pp., 2008.

  37. F. Wiedijk, "De kunst van het bewijzen." In: Wiskunde en profil, Het gezicht van de wiskunde, Vakantiecursus 2008, CWI syllabus 58, 107-130, 2008: ps.gz pdf dvi tex

    Abstract: ps.gz pdf dvi tex [23 pp.]

  38. C. Kaliszyk, F. van Raamsdonk, F. Wiedijk, H. Wupper, M. Hendriks & R. de Vrijer, "Deduction using the ProofWeb system", report ICIS-R08016, 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.]

  39. 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. Skaf-Molli & 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 fully-fledged 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.]

  40. F. Wiedijk, "Formal proof - getting started", Notices of the AMS 55(11), 1408-1414, 2008: ps.gz pdf dvi tex

    No abstract. [13 pp.]

  41. F. Wiedijk, "Formalizing Arrow's theorem", Sadhana 34(1), 193-220, 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.]

  42. F. Wiedijk, "Practising logic through the web", Nieuwsbrief van de NVTI, 13, 61-68, 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.]

  43. 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, 197-200, 2009: ps.gz pdf dvi tex

    No abstract. [1 p.]

  44. M. Niqui & F. Wiedijk, "`Many Digits' Friendly Competition", report ICIS-R09007, 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.]

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

  46. C. Tankink, H. Geuvers, J. McKinna & F. Wiedijk, "Proviola: a Tool for Proof Re-animation". 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, 440-454, 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 frame-by-frame 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.]

  47. 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 Meta-languages: Theory and Practice, EPTCS 34, 53-67, 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 pseudo-terms.
    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 well-typed 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.]

  48. F. Wiedijk, "Stateless HOL". In: T. Hirschowitz (ed.), Types for Proofs and Programs, TYPES 2009, Revised Selected Papers, EPTCS 53, 47-61, 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.]

  49. 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, 301-303, 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.]

  50. 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.

  51. F. Wiedijk, "Pollack-inconsistency". In: C. Sacerdoti Coen & D. Aspinall, UITP 2010, 9th International Workshop on User Interfaces for Theorem Provers, ENTCS 285, 85-100, 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 pseudo-terms.
    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 well-typed 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.]

  52. F. Wiedijk, A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving. Logical Methods in Computer Science 8(1), 1-26, 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.]

  53. F. Wiedijk, "Handbook of Practical Logic and Automated Reasoning," by John R. Harrison, Cambridge University Press, 2009. Journal of Automated Reasoning 49(1), 107-109, 2012: ps.gz pdf dvi tex

    No abstract. [3 pp.]

  54. R. Krebbers & F. Wiedijk, Separation Logic for Non-local Control Flow and Block Scope Variables. In: F. Pfenning (ed.), Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, LNCS 7794, 257-272, 2013: ps.gz pdf dvi tex

    Abstract. We present an approach for handling non-local 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 C-like 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.]

  55. F. Wiedijk, "A large routine." In: Inge Bethke, Bert Bredeweg & Alban Ponse (eds.), Liber Amicorum voor / for Jan A. Bergstra, Informatics Institute, University of Amsterdam, 162-163, 2016: pdf tex (version in the Liber: pdf)

    Abstract. This is a short text that I wrote for the Liber Amicorum for Jan Bergstra, presented at his retirement in December 2016. It speculates about a program that Alan Turing wrote in 1949.
    The version for the Liber used a tiny font and very long lines to fit everything on the two pages I had available. This is a version with a more reasonable layout. It also has references, and an added appendix with the source code of the program. [6 pp.]


publications notes mizar talks

(last modification 2017-05-23)