Talks

"Reflection with partial functions", Tsukuba University, 2000-01-25.

Abstract. I'll describe a method that we developed in a project of Henk Barendregt and Herman Geuvers where we are formalizing a proof of a non-trivial mathematical theorem (the "fundamental theorem of algebra") using the Coq system from France. When formalizing mathematical proofs in a computer, two things generally are difficult: (1) reasoning in a "human" way and, (2) "doing algebra", i.e., calculating with expressions. My talk is about the second difficulty. However, the method that I'll describe is rather specific to the "type theoretical" way of checking proofs (so it's specific to systems like Coq.)
In order to generate proofs algorithmically, in type theory one can use a standard method called "reflection" or "the two level approach". For instance the "Ring" tactic of Coq uses this method. We wanted to extend this tactic to include division, and ran into the problem that expressions involving division can be undefined: division is a partial function. The solution we found was to use an interpretation relation instead of an interpretation function. In this way a tactic called "Rational" was written, that we are currently using in our project.
I'll begin the talk with a general introduction into proof checking of mathematics and will present a short overview of various projects: Automath, Mizar, QED, and the type theoretical systems like Agda, Lego and Coq. [1+24 slides]
"Computer algebra met condities?", University of Nijmegen, 2000-05-08.

Abstract. De huidige generatie computer algebra systemen beantwoordt niet het soort vragen dat bij proof-checken optreedt. Analyse van de "calculus" berekeningen in een voorbeeld van een computerbewijs, toont dat deze gebruik maken van eerdere vergelijkingen uit de bewijsgang. Omdat dit soort "condities" niet kan worden ingevoerd (en dus niet gebruikt) in pakketten als Maple en Mathematica, is de huidige computer algebra minder bruikbaar voor proof-checken dan je zou verwachten. [in Dutch, 1+20 slides]
"Mizar, a not very well known proof tool", Proof Tool Day, University of Ghent, 2000-05-26, 14:00: html

Abstract. The Mizar system from Poland is mentioned often, but not many people know it from first hand experience. It is special in the sense that it uses declarative proofs, in contrast to the procedural proofs of most other proof tools. A short overview of the history of proof checking will be followed by an introduction to the Mizar system, and an assessment of its strengths and weaknesses. [1+16 slides]
"The de Bruijn factor", TPHOLs 2000 (poster), Portland, 2000-08-15.

No abstract. [2 slides]
"Kneser's proof of the fundamental theorem of algebra without rational numbers", TYPES 2000, Durham, 2000-12-08.

Abstract. In Nijmegen we formalize in Coq a constructive proof of the fundamental theorem of algebra, due to Kneser. The original proof makes use of the decidability of the rational numbers, but we decided to change it such that it didn't refer to the rational numbers anymore. One motivation for this was that our formalization has the real numbers axiomatically (they are not built from the rationals.) We also think that the new proof is more natural, because one doesn't have to switch between rational and real numbers. Although the adaptation of the proof has never been looked at by other mathematicians, we can be sure it is correct, because we formalized it in Coq.
This is joint work with Herman Geuvers and Jan Zwanenburg. [1+12 slides]
"The algebraic hierarchy of the FTA project", LRI, Orsay, 2001-02-02.

No abstract. [1+25 slides]
"The algebraic hierarchy of the FTA project", Calculemus 2001, Siena, 2001-06-21.

No abstract. [1+12 slides]
"Mizar Light for HOL Light", TPHOLs 2001, Edinburgh, 2001-09-06.

No abstract. [1+15 slides]
"A contemporary implementation of Automath", 35 years of Automath workshop (invited talk), Heriot-Watt University, Edinburgh, 2002-04-10, 16:00: advi tex

Abstract. This talk presents "aut", a modern Automath checker. It is a straight-forward reimplementation of the Zandleven Automath checker from the seventies. It was implemented about five years ago in the programming language C. It knows 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 noticable features:
- It is fast. It is 30 times as fast as Mizar, which itself is 30 times as fast as Coq. On a 1GHz machine it will check the full Jutting formalization (about 750K of Automath source) in 0.5 seconds.
- Its implementation of lambda terms doesn't use named variables or de Bruijn indices (the two common approaches) but instead uses a directed graph representation. In this, bound variables are represented by pointers to a lambda.
The program has the feature that it can compile an Automath text into one very 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.) [1+20 slides]
"The Fundamental Theorem of Algebra", 35 years of Automath workshop (invited talk, for Herman Geuvers), Heriot-Watt University, Edinburgh, 2002-04-13, 16:00.

Abstract. The Fundamental Theorem of Algebra states that every polynomial over the complex numbers has a root. In Nijmegen we have formalised a constructive proof of this theorem in Coq. In this project, we wanted to also set up a library of results (about reals and complex numbers and polynomials) that could be re-used, by us and by others. We have therefore defined an algebraic hierarchy of monoids, groups, rings and so forth that allows to prove generic results and use them for concrete instantiations.
In the talk I will briefly outline the FTA project. The main part will consist of an outline of the algebraic hierarchy and its use. This part will contain an explanation of the basic features of Coq. [1+20 slides]
"The constructive core of HOL Light in Coq", TYPES 2002, Nijmegen, 2002-04-28, 12:00 & LRI, Orsay, 2002-06-28, 13:30: advi tex

Abstract. In order to be able to translate HOL proofs to Coq, we have looked for a set of classical axioms that would allow one to encode the HOL logic in Coq. A naive attempt at such an axiomatization turned out to be inconsistent with Coq, because of the impredicativity of Set.
However, we did find a semantics for the constructive part of the HOL Light logic in Coq (without having to put any axioms on top of the Calculus of Inductive Constructions.) In this semantics a HOL type corresponds to a setoid in Type, and in particular the HOL bool type corresponds to the Omega setoid (Prop with logical equivalence.)
The constructive core of HOL Light exactly fits this semantics, apart from the HOL type definition mechanism. We present a different mechanism to define new types, which does fit the semantics, but this turns out to be too weak to construct types like the natural numbers and cartesian products inside the HOL logic. [1+14 slides]
"The meaning of infinity in calculus and computer algebra systems", Calculemus 2002, Marseille, 2002-07-03, 14:00: advi 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.
We stress the need to have a proper semantics for computer algebra expressions, especially if one wants 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. [1+14 slides]
"Formalizing mathematics in the computer", Leiden University, 2002-10-10, 16:00: advi tex

Abstract. I will present "formal mathematics". This field studies how to verify the correctness of mathematical theories with the computer. I will discuss the reliability and the feasibility of this endeavor. At the end of the talk I will show a small formalization in the Mizar proof system. [1+24 slides]
"A model for Delta-Lambda?", local seminar, University of Nijmegen, 2003-02-03, 13:30.

Abstract. De Bruijn's type theory "Delta-Lambda" is an interesting logical framework similar to lambda-P, but in some respects fundamentally different and maybe simpler and more elegant. The system lambda-P has a straight-forward set theoretical model, and there is substantial theory about its use as a logical framework. For Delta-Lambda no similar model or theory are known, which may be the reason Delta-Lambda has never got the attention it deserves.
I have adapted a model that was shown by Dana Scott at the TYPES workshop last year for Delta-Lambda. However until now I haven't been able to prove the theorem that states that it actually is a model, so I will just define the model and state the theorem without proof. I also will indicate how the model might be used to show that Delta-Lambda is adequate as a logical framework for first order logic. [no slides]
"Comparing mathematical provers", MKM 2003, University of Bologna, Bertinoro, 2003-02-18, 11:30: advi tex

No abstract. [1+13 slides]
"A Mizar mode for Coq?", Math-in-Coq meeting, LRI, Orsay, 2003-04-24, 09:30: advi tex

Abstract. First I'll explain what a "Mizar mode" is. Then I'll show my Mizar mode for the HOL Light system. Finally I'll tell what is the main unsolved problem (according to my experience with my HOL Light Mizar mode) that is in the way of having a Mizar mode for Coq. [1+28 slides]
"Formal proof sketches and MoWGLI", Proof Tools Day 2003, CWI, Amsterdam, 2003-04-25, 14:30: advi tex

Abstract. Proofs that can be checked by a proof assistant generally look like a long stream of unreadable "code", which doesn't at all resemble the way that the proof would be presented to a human being. A possible solution to this problem that exists for several systems is to generate natural language from the formal proof. However, this has two disadvantages: first, one separates the "input format" that one interacts with when creating or modifying the proof from the "output format" that is not directly editable, and second, such a natural language representation is computer-generated and therefore not as easily readable as text that has been written by a human (who knows what are the essential steps in the proof and what are irrelevant details.)
We propose a different approach to the problem of making a formalization accessible. We define a variant of a declarative proof language that allows one to write "formal proof sketches". 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 a full formal proof.
We will show through examples that formal proof sketches can be very close to natural language proofs that one finds in actual mathematical textbooks. We will also show that it is easy to relate a formal proof sketch to the corresponding completed formalization. This means that that formal proof sketches can be used to "navigate" a full formal proof.
We will finally show computer-generated natural language from the HELM system next to a corresponding human-written formal proof sketch, to compare the two approaches to making formalizations accessible. [1+15 slides]
"Formal proof sketches & Lamport-style proofs", TYPES 2003, Torino, 2003-05-03, 11:00: advi tex

Abstract. In his "How to Write a Proof", Leslie Lamport presented a method for the development of hierarchical proofs using top-down refinement. His approach has been implemented in the IMP project of Paul Cairns and Jeremy Gow. They created on-line topology course notes in which the proofs can be interactively browsed in Lamport's format.
A related way of presenting a proof is through a "formal proof sketch". In a formal proof sketch one uses the proof language of the Mizar system, but leaves out many of the proof steps and most of the references between steps that are needed to turn it into a fully checkable Mizar formalization. In contrast with Lamport's proofs, formal proof sketches look similar to the proofs of ordinary textbook mathematics.
In this talk I will compare both proof styles. I will present some examples, and will discuss the main differences between the two approaches. [1+15 slides]
"John Harrison's formalization of the AKS primality test", Intercity Number Theory Seminar, Nijmegen, 2003-06-06, 16:00: advi tex

Abstract. This talk will present work of John Harrison, as a showcase of what formalization of elementary number theory can look like. The work that will be shown is a formalization in the HOL Light system of the proof of theorem 2.3 from Bernstein's "proving primality after Agrawal-Kayal-Saxena".
The talk will explain the foundations of HOL Light, then it will present various examples of how mathematical notions can be defined inside this system, and finally it will show the AKS formalization, discussing one of the files in some detail and then focusing within this file on one of its lemmas. [1+25 slides]
"Partial functions & domain conditions", TPHOLs 2003, Rome, 2003-09-11, 09:30: advi tex

No abstract. [1+16 slides]
"A Mizar mode for Coq by Mariusz Giero", MoWGLI meeting, INRIA, Sophia-Antipolis, 2003-09-16: advi tex

No abstract. [4 slides]
"Formal proof sketches", INRIA, Sofia-Antipolis, 2003-09-17, 14:30: advi tex

Abstract. Proofs that can be checked by a proof assistant generally look like a long stream of unreadable "code", which doesn't at all resemble the way that the proof would be written by a human being.
A possible solution to this problem, which exists for several systems, is to generate natural language text from the formal proof. However, such a natural language representation itself generally looks like a long stream of unreadable "computer generated text", and doesn't much resemble the way that the proof would be written by a human being either.
People often seem to think that by using a "folding interface" in which one can hide parts of this generated text, this situation will become manageable, but I'll argue that this is not the case.
In my talk I will propose a different approach to the problem of making a formalization accessible. I will define a variant of a declarative proof language that allows one to write "formal proof sketches". 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.
I will show through examples that if one writes a formal proof sketch of an existing mathematical proof, then this formal proof sketch will be very similar to the informal original. [1+25 slides]
[merged from 17 and 18]
"A comparison of foundations of mathematics", local seminar, University of Nijmegen, 2003-11-10, 11:00: advi tex

No abstract. [1+30 slides]
"Bewijzen in de computer", Nationale Wiskunde Dagen, Noordwijkerhout, 2004-02-06, 16:15: advi pdf tex

Abstract. Een eeuwenoude droom is om de hele wiskunde expliciet uit een handvol axioma's af te leiden. Dit probeerden bijvoorbeeld Whitehead en Russell in hun Principia Mathematica. Maar het bleek altijd weer een niet realistische onderneming. Er zijn gewoon veel te veel details. Zo kost het in de Principia Mathematica honderden pagina's om 1 + 1 = 2 af te leiden, en veel verder dan dat komt het dan ook niet. Maar nu met de komst van de computer is dit eindelijk veranderd! Nu maakt de computer het wel mogelijk om echt verder te komen dan 1 + 1 = 2. De computer kan namelijk alles netjes bijhouden en zelfs simpele details zelf invullen. En er bestaan nu dus systemen met wiskundige bibliotheken waarin niet-triviale wiskundige stellingen in volledig detail uit de axioma's van het systeem worden afgeleid.
Wiskunde gaat over berekenen en bewijzen. Bij berekenen gaat het om het wat, om het antwoord, en bij bewijzen gaat het om het waarom, om het begrip. Tegenwoordig lijkt het er soms op dat bewijzen een uitstervend ambacht is, maar in de informatica zijn ze helemaal niet uitgestorven, de bewijzen. Integendeel! Daar worden ze gebruikt om te laten zien dat chips of computerprogramma's foutloos zijn. Om deze "informatica bewijzen" te controleren zijn er een aantal systemen gebouwd, en die worden ook gebruikt om wiskunde mee te doen.
Een wiskundig bewijs zo opschrijven dat de computer het kan nalopen combineert het beste van twee werelden: programmeren en wiskunde. Het is als het schrijven van een computerprogramma, maar je weet zeker dat er geen "bugs" in zitten. En het gaat over wiskunde, maar je hoeft je niet af te vragen of je het wel echt begrepen hebt, want de computer houdt je eerlijk. Een bewijs in de computer coderen is als het spelen van een geweldig computerspel: als de stelling is helemaal is bewezen voelt het alsof je een "level" hebt uitgespeeld. Het is als het doen van hele mooie, hele ingewikkelde puzzels. En het gaat dan nog ergens over ook! [in Dutch, 1+22 slides]
"Mathematical ontology", MoWGLI & Authomath meeting, DFKI, Saarbrücken, 2004-03-23, 10:00: advi tex

No abstract. [1+11 slides]
"When will it happen?", Automath Digital Archive Opening Symposium, University of Eindhoven, 2004-05-26, 15:10: advi tex

Abstract. The basic idea behind Automath was to develop a "justification system" (as De Bruijn calls it in his 1991 overview article). Since the start of Automath there have been many efforts to reach goals similar to Automath: many "justification systems" have been defined, implemented and tested on real mathematical examples. We give an overview of the goals of Automath and its heritage and we try to find out where we stand in the development of an ideal justification system and which challenges lie ahead. [1+10 slides]
"Convertibility proof terms", local seminar, University of Nijmegen, 2004-06-14, 14:00 & LFM'04, IJCAR 2004 workshop, Cork, Ireland, 2004-07-05 & local seminar, Free University, 2004-11-19, 15:15: advi tex

Abstract. The type theory lambda-P corresponds to the logical framework LF. 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. [1+14 slides]
"Integrating procedural and declarative proof", small TYPES workshop, University of Nijmegen, 2004-11-01, 15:00: advi tex

Abstract. We describe an approach for merging the two different proof styles found in state-of-the-art proof assistants: the procedural style (originating from LCF and found in for example the HOL and Coq systems) and the declarative style (originating from Mizar and also found in the Isar proof language of the Isabelle system).
Our approach consists of identifying the subgoals of the procedural proof styles with incomplete declarative proofs. One starts with an empty declarative proof. Then one modifies this incomplete proof either in a procedural or a declarative way. Either one applies a tactic to a step in the proof that has not been justified yet, or one manually modifies the proof and then rechecks it.
Our approach is an improvement over a similar way of generating proofs that is found in the ALF/Agda systems. We work with declarative proofs in which the steps correspond to the steps in a tactic-style proof, instead of having declarative proofs in which the steps correspond to the basic inference steps of the foundation of the system.
Our approach also is an improvement over the declarative proofs that one finds in the Isabelle/Isar system. There one needs to write the statements in the steps of the proof oneself. Using our approach these statements will be inserted into the proof automatically by the tactics. Also in our approach there will be a one-to-one relationship between the tactics and the justifications in the proof, removing the need to have "methods" of Isabelle/Isar.
A prototype of our approach implemented on top of the HOL Light system is up and running and will be shown. [1+15 slides]
"logical verification", slides for a graduate course type theory and Coq, Free University, Amsterdam, 2004-09-08 - 2004-12-01: pdf 01 02 03 04 05 06 07 08 09 10 11 12 advi 01 02 03 04 05 06 07 08 09 10 11 12 tex 01 02 03 04 05 06 07 08 09 10 11 12

No abstract. [12+380 slides]
"Proof assistants for mathematics", OzsL Schoolweek, Nunspeet, 2004-12-02, 15:30: advi tex

Abstract. In this lecture we will present an overview of the main proof assistants for doing mathematical proof in the computer. Then we will zoom in on two specific proof assistants: the procedural system called HOL, and the declarative system called Mizar. In both of these systems we will show how to develop a small proof. [1+36 slides]
"Onderzoek, onderwijs, organisatie", sollicatie Universitair Docent bij Grondslagen, 2004-12-06, 15:00: advi pdf tex

No abstract. [in Dutch, 1+15 slides]
"STTwU in Coq", TYPES 2004, Paris, 2004-12-15, 15:10: advi tex

Abstract. When one considers the foundations of a classical proof assistant like HOL, it has various "features" that one doesn't have in a constructive framework: (1) the law of the excluded middle, (2) extensional equality, and (3) a choice operator (which for any predicate returns an object that satisfies the predicate, if there is one.) To model such a system in a constructive world it seems that one cannot avoid having to add "axioms" to obtain these features.
However, for the theory - introduced by William Farmer - called "STTwU" (simple type theory with undefinedness), this turns out not to be the case. This theory is classical, extensional, and it has a choice operator, but it can be mapped into a constructive world without having to add any axioms.
In this talk we will both present a LF context corresponding to STTwU, as well inhabit that context in Coq. We use a stack of tricks to do this: a double negation translation for the classical logic, setoids for the extensionality, partial setoids to deal with undefinedness, and finally dual setoids for the choice operator.
Our work shows that we can have the classical world of STTwU and still consider our work meaningful to constructive mathematicians. [1+8 slides]
"Integrating Coq-style and Mizar-style proof", small TYPES workshop, LAMA, Université de Savoie, 2005-04-13, 11:30: advi tex

Abstract. There are roughly speaking two proof styles that one finds in proof assistants. If one wants the proof script that one works on to be readable, and to have it look similar to informal mathematics, then there is the declarative proof style of for instance the Mizar and Isar systems. On the other hand if one wants the proof assistant to automate as much as possible, there is the procedural proof style in which the proof script is just a list of tactics, which originated with the LCF system. We will present a synthesis between these two approaches, where both the tactics script and the subgoals that it passes through are continuously merged into a single declarative proof. We will present this "best of two worlds" proof style, and give a small demo of a prototype implemented on top of the HOL Light system. [1+15 slides]
"Formalization of mathematics", TYPES Summer School 2005, Göteborg, 2005-08-23, 11:10 & seminar Algebraic and Numerical Algorithms and Computer-assisted Proofs, Dagstuhl, 2005-09-27, 17:10: advi pdf tex

No abstract. [1+51 slides]
"Computer algebra inside a proof assistant", small TYPES workshop, Nijmegen, 2005-10-03, 15:30: advi tex

Abstract. The MathXpert computer algebra system is one of the few computer algebra systems that tries to be logically sound. It implements basic algebra and analysis on the high school level, and for educational purposes is as faithful to high school textbooks as possible.
MathXpert gives its users 1702 "operations" that can be applied to expressions inside the system. We will show that it is easy to mimic the MathXpert architecture inside the HOL Light proof assistant, so that one gets MathXpert-style "operations" available there as well, but with the advantage that they also generate proofs, so that the correctness of the algebraic manipulations will be guaranteed by the proof assistant. [1+16 slides]
"An introduction to the formalization of mathematics and decision procedures", Diamant day, Nijmegen, 2005-10-28, 11:15: advi tex

Abstract. This talk is an introduction to formalization of mathematics and decision procedures. The current state of the art in formalization of mathematics will be presented. After that we will argue that "decision procedures" (which are algorithms that each solve a specific class of mathematical problems) is the most important technology to make formalization of mathematics more practical than it is today. An overview of the most important currently available decision procedures will then be given. [1+31 slides]
"the Poincaré principle versus reduction in the logic", TYPES 2006, Nottingham, 2006-04-19, 14:00: advi tex

Abstract. For many people an important reason to prefer type theory over axiomatic set theory is that it satisfies what Henk Barendregt calls "the Poincaré principle". This principle states that "calculations do not need to be proved" (most type theoretical proof assistants satisfy this principle because in these systems calculations are done automatically by term reduction in the kernel; this reduction implements the conversion rule of the underlying type theory). I will argue that this difference between type theory and axiomatic set theory is not as important as it is generally made out to be, by showing that one can have the Poincaré principle in a natural way in ZFC set theory as well. [1+12 slides]
"Functional programming in practice", course Principles of Programming Languages, Free University Amsterdam, 2006-05-11, 11:00: advi pdf tex

No abstract. [1+9 slides]
"How to implement a typechecker?", CHIT/CHAT workshop, University of Nijmegen, 2006-12-19, 11:05: advi pdf tex

Abstract. The litmus test of whether a programming language is any good is that its compiler has been written in the language itself. That is, the compiler should be able to compile itself. Similarly, the litmus test for a proof assistant should be that it has formally verified the correctness of its own proof checking kernel. This talk will present an overview of what already has been done in this direction, and address the question of what is the best approach to make it practical to formally verify the actual source code of a proof assistant. The main purpose of this talk will be to encourage discussion on this topic by the audience of the CHIT/CHAT workshop. [1+19 slides]
"Formalization of mathematics", Nederlands Mathematisch Congres, Leiden University, 2007-04-12, 11:45: advi pdf ps.gz tex

Abstract. "Formalization" is the encoding of mathematics in a computer in sufficient detail that a computer program can check the correctness without further human assistance. Systems for the development and verification of formalized mathematics are called "proof assistants". This talk will introduce the most interesting proof assistants of the moment, and then present the state of the art of formalization of mathematics, including the formalization of the four color theorem, the Flyspeck project for the formalization of the proof of the Kepler conjecture, and the current work at the joint research institute of Microsft and INRIA in Paris. [1+26 slides]
"Do not take natural language too seriously", Seminar Formal Mathematics, University of Bonn, 2007-04-17, 13:00: advi pdf ps.gz tex

No abstract. [1+4 slides]
"The Mizar type system", TPHOLs 2007, University of Kaiserslautern, 2007-09-12, 10:00: advi pdf ps.gz 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. [1+16 slides]
"How to build a library of formalized mathematics", MathWiki Workshop, University of Edinburgh, 2007-10-31, 11:00: advi pdf ps.gz tex

Abstract. I will discuss what I perceive to be the main reasons that there is not yet a large scale effort to create a good and comprehensive library of formal mathematics. [1+16+7 slides]
"ProofWeb: logic education through the web", FORMED 2008, Budapest, 2008-03-29, 15:20: advi pdf tex

No abstract. [1+10 slides]
"Statistics on digital libraries of mathematics", MKM 2008, CICM 2008, Birmingham, 2008-07-28, 12:00: advi pdf ps.gz tex

Abstract. We present statistics on the standard libraries of four major proof assistants for mathematics: HOL Light, Isabelle/HOL, Coq and Mizar. [1+15 slides]
"De kunst van het bewijzen", CWI vakantiecursus wiskunde 2008, Technische Universiteit Eindhoven, 2008-08-23, 14:15: advi pdf ps.gz tex

Abstract: ps.gz pdf dvi tex [1+29 slides]
"Merging the procedural and declarative proof styles", MAP 2008, Trieste, 2008-08-25, 14:00 & Mathematical Logic and Computers, satellite workshop of ALC 10, Kobe, Japan, 2008-08-31, 14:50: advi pdf ps.gz tex

Abstract. Proof assistants for the formalization of mathematics currently use two very different proof styles. Declarative systems like Mizar use a textual input format that is close in style to informal mathematics. This input then is only passively checked by the system. Procedural systems like HOL and Coq use an interactive proof style where the system displays proof obligations called "goals", which the user then reduces by executing "tactics". In a procedural proof assistant the scripts that are the "proofs" just consist of sequences of those tactics, and are not readable as normal text.
In the Isabelle proof assistant both the procedural and declarative interaction styles are available in a single system. In Isabelle often the outline of the proof is written declaratively, after which the details are filled in procedurally. However, in Isabelle the two proof styles still are separate.
In this talk an interaction model will be presented in which the declarative and procedural styles have been truly merged. This leads to a proof language that is very portable. Currently existing procedural and declarative proofs both will be automatically convertible to such a system. This even holds for proofs from different proof assistants, and even for proofs from proof assistants based on different foundations.
A proof assistant implementing this merged interaction model is currently being developed on top of John Harrison's HOL Light system. This effort will be described, and the current state of the prototype will be demoed. [1+29 slides]
"Avoiding state with infinite contexts", ALC 10, Kobe, Japan, 2008-09-05, 15:40 & local seminar, University of Nijmegen, 2008-09-09, 15:45: advi pdf ps.gz tex

Abstract. Proof assistants are computer programs that verify the correctness of mathematics. Such a program generally has a state, of which an essential part is a table that holds the defined symbols that so far have been introduced in the mathematics. Logically that part of the state corresponds to the contexts that occur in the logical derivations that represents the mathematics that is being verified. In most logical systems free variables in the statements are not accounted for in the contexts of the judgements. However, in type theory it is customary to administer these variables in the contexts as well. In this talk we will go to the other extreme and present a version of type theory in which there are no explicit contexts. All variables (even the variables that correspond to assumptions) are treated as free. In some sense they are still being bound, but in an infinite context.
This logical system inspires an implementation approach for LCF style proof assistants where the logical core of the system no longer needs state. (For this approach it is essential that the programming language supports testing for pointer equality, to allow fast equality checking.)
We present two prototypes of a logical core for a proof assistant using this approach. The first is a version of John Harrison's HOL Light system in which state has been removed from the logical core. This change allows the system to support "undoing" definitions in a logically sound way. The second is an implementation of a Pure Type System in LCF style. [1+18 slides]
"Formalizing Arrow's theorem in Mizar", ILLC, University of Amsterdam, 2009-03-06, 16:00: advi pdf ps.gz tex

Abstract. Some time ago the Mizar system for formal mathematics was used to "formalize" a small proof of Arrow's theorem by John Geanakoplos. This talk describes formalization of mathematics in general, and also presents specifics of the Mizar formalization of Arrow's theorem. In particular two questions are addressed: whether errors were found in the proof by Geanakoplos, and more in general, whether formalization can be useful outside of mathematics. [1+34 slides]
"Het servetje van Hendrik Lenstra", guest lecture in the "Kaleidoscoop 2" course, Utrecht University, 2009-03-12, 14:15: advi pdf ps.gz tex

No abstract. [in Dutch, 1+24 slides]
"Sketching Lagrange", local seminar, University of Nijmegen, 2009-06-09, 15:45: advi pdf ps.gz tex

Abstract. We illustrate the methodology of Formal Proof Sketches by showing a small Mizar formalization of Lagrange's theorem, which states that the order or a subgroup always divides the order of the group. [1+27 slides]
"Three wishes", future of ITP workshop, University of Cambridge, 2009-08-24, 09:30: advi pdf ps.gz tex

Abstract. I will outline three systems that I imagine I would like using, but of which I do not know whether they exist. They are: (1) a nice proof assistant for mathematics, (2) a nice proof environment for ML program correctness, and (3) a nice proof environment for C program correctness. I'll describe for each of these systems what they are like in my imagination, and in each case what I think is the primary reason they don't exist in that form yet. [1+12 slides]
"Two automation challenges", Dagstuhl seminar "interaction versus automation", 2009-10-06, 17:00: advi pdf ps.gz tex

Abstract. We present two challenges for the automation of mathematics. The first challenge is to automate the mathematical reasoning steps that in a non-formalized mathematical textbook are just explained with the word "therefore". The second challenge is to automate mathematics at the high school level. We propose a project to combine these challenges and make them specific. [1+15 slides]
"Trust", 3SWeb project meeting, MLstate, Paris, 2009-10-19: advi pdf ps.gz tex

No abstract. [1+1 slides]
"Formal proof with the computer", Johann Bernoulli Colloquium, University of Groningen, 2010-03-17, 16:15: advi pdf ps.gz tex

Abstract. An overview of the state of the art in computer checked proofs, both in mathematics and computer science, will be presented. After that the main limitations of current systems for computerized proof development will be discussed. [1+33 slides]
"Pollack-inconsistency", UITP 2010, Edinburgh, 2010-07-15, 12:00: pdf ps.gz dvi tex

No abstract. [8+17 slides, 95 pauses]
"The next generation of proof assistants: ten questions", LSFA 2010, Natal, Brazil, 2010-08-31, 16:30 & local seminar, University of Nijmegen, 2012-03-13, 10:45: pdf ps.gz dvi tex

Abstract. We will discuss the strengths and weaknesses of present day proof assistants and try to clarify what the next generation should be like, by asking ten questions to the audience. [32 slides, 234 pauses]
"miz3: an experiment in proof assistant interaction style", local seminar, University of Nijmegen, 2012-05-29, 10:45.

Abstract. I'll present my experimental miz3 proof interface to the HOL Light proof assistant. It attempts to integrate the "declarative" interaction style of Mizar and Isar with the "procedural" interaction style of systems that stem from the LCF tradition, like Coq and HOL. [no slides]
"Should proof assistants be used to verify absence of overflow?", local seminar, University of Nijmegen, 2013-03-12, 13:30.

No Abstract. [no slides]
"Some unfinished projects", local seminar, University of Cambridge, 2013-08-14, 13.00.

Abstract. I'll present a few projects that I'm considering/working on/involved with:
[no slides]
"(Co)verifying a compiler and a prover: the CakeML project", local seminar, University of Nijmegen, 2013-10-29, 13:30: pdf tex

Abstract. I will summarize what I learned during my visit to Cambridge about the CakeML project of Ramana Kumar, Magnus Myreen, Michael Norrish and Scott Owens, and the related verification of the HOL Light kernel. [1+12 supplementary slides]

publications notes mizar talks

(last modification 2013-10-29)