"Reflection with partial functions", Tsukuba University, 2000-01-25.
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
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.
"Computer algebra met condities?", University of Nijmegen, 2000-05-08.
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
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.
"Kneser's proof of the fundamental theorem of algebra without rational numbers", TYPES 2000, Durham, 2000-12-08.
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.
"The algebraic hierarchy of the FTA project", LRI, Orsay, 2001-02-02.
"The algebraic hierarchy of the FTA project", Calculemus 2001, Siena, 2001-06-21.
"Mizar Light for HOL Light", TPHOLs 2001, Edinburgh, 2001-09-06.
"A contemporary implementation of Automath", 35 years of Automath workshop (invited talk), Heriot-Watt University, Edinburgh, 2002-04-10, 16:00: advi tex
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.
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
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
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
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.
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.
"Comparing mathematical provers", MKM 2003, University of Bologna, Bertinoro, 2003-02-18, 11:30: advi tex
"A Mizar mode for Coq?", Math-in-Coq meeting, LRI, Orsay, 2003-04-24, 09:30: advi tex
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
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.
"Formal proof sketches & Lamport-style proofs", TYPES 2003, Torino, 2003-05-03, 11:00: advi tex
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.
"John Harrison's formalization of the AKS primality test", Intercity Number Theory Seminar, Nijmegen, 2003-06-06, 16:00: advi tex
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.
"Partial functions & domain conditions", TPHOLs 2003, Rome, 2003-09-11, 09:30: advi tex
"A Mizar mode for Coq by Mariusz Giero", MoWGLI meeting, INRIA, Sophia-Antipolis, 2003-09-16: advi tex
"Formal proof sketches", INRIA, Sofia-Antipolis, 2003-09-17, 14:30: advi tex
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
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
[merged from 17 and 18]
"A comparison of foundations of mathematics", local seminar, University of Nijmegen, 2003-11-10, 11:00: advi tex
"Bewijzen in de computer", Nationale Wiskunde Dagen, Noordwijkerhout, 2004-02-06, 16:15: advi pdf tex
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
"When will it happen?", Automath Digital Archive Opening Symposium,
University of Eindhoven, 2004-05-26, 15:10: advi tex
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.
"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
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.
"Integrating procedural and declarative proof", small TYPES workshop, University of Nijmegen, 2004-11-01, 15:00: advi tex
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.
"logical verification", slides for a graduate course type theory and Coq, Free University, Amsterdam, 2004-09-08 - 2004-12-01:
"Proof assistants for mathematics", OzsL Schoolweek,
Nunspeet, 2004-12-02, 15:30: advi tex
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.
"Onderzoek, onderwijs, organisatie", sollicatie Universitair Docent bij Grondslagen, 2004-12-06, 15:00: advi pdf tex
[in Dutch, 1+15 slides]
"STTwU in Coq", TYPES 2004, Paris, 2004-12-15, 15:10: advi tex
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
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
"Integrating Coq-style and Mizar-style proof", small TYPES workshop, LAMA, Université de Savoie, 2005-04-13, 11:30: advi tex
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.
"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
"Computer algebra inside a proof assistant", small TYPES workshop, Nijmegen, 2005-10-03, 15:30: advi tex
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
"An introduction to the formalization of mathematics and decision procedures", Diamant day, Nijmegen, 2005-10-28, 11:15: advi tex
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.
"the Poincaré principle versus reduction in the logic", TYPES 2006, Nottingham, 2006-04-19, 14:00: advi tex
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.
"Functional programming in practice", course Principles of Programming Languages, Free University Amsterdam, 2006-05-11, 11:00: advi pdf tex
"How to implement a typechecker?", CHIT/CHAT workshop, University of Nijmegen, 2006-12-19, 11:05: advi pdf tex
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.
"Formalization of mathematics", Nederlands Mathematisch Congres, Leiden University, 2007-04-12, 11:45: advi pdf ps.gz tex
"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.
"Do not take natural language too seriously", Seminar Formal Mathematics, University of Bonn, 2007-04-17, 13:00: advi pdf ps.gz tex
"The Mizar type system", TPHOLs 2007, University of Kaiserslautern, 2007-09-12, 10:00: advi pdf ps.gz tex
In Mizar, unlike in most other proof assistants,
the types are not part of the foundations of the
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
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.
"How to build a library of formalized mathematics", MathWiki Workshop, University of Edinburgh, 2007-10-31, 11:00: advi pdf ps.gz tex
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.
"ProofWeb: logic education through the web", FORMED 2008, Budapest, 2008-03-29, 15:20: advi pdf tex
"Statistics on digital libraries of mathematics", MKM 2008, CICM 2008, Birmingham, 2008-07-28, 12:00: advi pdf ps.gz tex
We present statistics on the standard
libraries of four major proof assistants for mathematics:
HOL Light, Isabelle/HOL, Coq and Mizar.
"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
"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
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
"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
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
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
"Formalizing Arrow's theorem in Mizar", ILLC, University of Amsterdam, 2009-03-06, 16:00:
advi pdf ps.gz tex
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.
"Het servetje van Hendrik Lenstra", guest lecture in the "Kaleidoscoop 2" course, Utrecht University, 2009-03-12, 14:15:
advi pdf ps.gz tex
[in Dutch, 1+24 slides]
"Sketching Lagrange", local seminar, University of Nijmegen, 2009-06-09, 15:45:
advi pdf ps.gz tex
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.
"Three wishes", future of ITP workshop, University of Cambridge, 2009-08-24, 09:30:
advi pdf ps.gz tex
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.
"Two automation challenges", Dagstuhl seminar "interaction versus automation", 2009-10-06, 17:00:
advi pdf ps.gz tex
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.
"Trust", 3SWeb project meeting, MLstate, Paris, 2009-10-19:
advi pdf ps.gz tex
"Formal proof with the computer", Johann Bernoulli Colloquium, University of Groningen, 2010-03-17, 16:15:
advi pdf ps.gz tex
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.
"Pollack-inconsistency", UITP 2010, Edinburgh, 2010-07-15, 12:00:
pdf ps.gz dvi tex
[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
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.
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.
"Some unfinished projects", local seminar, University of Cambridge, 2013-08-14, 13.00.
I'll present a few projects that I'm considering/working on/involved with:
- The miz3 proof language for HOL Light
- A partial version of the HOL Light logic
- A Poincaré principle for HOL Light
- The CH2O project
"(Co)verifying a compiler and a prover: the CakeML project", local seminar, University of Nijmegen, 2013-10-29, 13:30: pdf tex
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]
(last modification 2013-10-29)