Small TYPES workshop
"Types for Mathematics / Libraries of Formal Mathematics"

slides of the talks are now available: see the program below

November 1-2 2004
Nijmegen NL

The workshop will be held at the campus of the Radboud University Nijmegen (formerly known as University of Nijmegen or Catholic University of Nijmegen).

Topics include, but are not limited to:

If you want to give a talk or a demo, please send a mail (with title and possibly abstract) to typesworkshop@cs.ru.nl.

Registration

The workshop will be free of charge. To register for the workshop send a mail to typesworkshop@cs.ru.nl.

The lunches (November 1 and 2) and the dinner (on November 1) have to be paid by the participants themselves. They will be organised by the organisation committee. The costs for each participant is:

If you want to take part in the lunches and dinner, please pay for them at the registration (Monday November 1). We can only take cash!

Please send a mail to typesworkshop@cs.ru.nl in case you are a vegetarian, so we can take that into account.

Program

The workshop will be held the 1st and 2nd of November. The first day the workshop will be located in the "Gymnasion". The second day the workshop will be located in the "Magnetenlab", near the "A" building, in room HFML 0220. (See the map below.)

Monday, November 1st

09:30-10:30   Robert L. Constable (invited speaker) Foundations for the Management of Formal Mathematical Knowledge [slides]
10:30   coffee
11:00-11:30   Clemens Ballarin Instantiation: Integrating Modules with Readable Proofs [slides]
11:30-12:00   Christian Urban Nominal Techniques as an Isabelle/HOL-Theory [slides]
12:00   lunch
14:00-14:30   Roland Zumkeller Towards a formal proof of the Kepler conjecture [slides]
14:30-15:00   Claudio Sacerdoti Coen A Coq tactic for one step conditional rewriting [slides]
15:00-15:30   Freek Wiedijk Integrating procedural and declarative proof [slides]
15:30   tea
16:00-16:30   Czeslaw Bylinski Strengthening the Computational Power of the Mizar Checker [slides]
16:30-17:00   Anna Zalewska Mizar Mathematical Library in Education [slides]
17:00   drinks
18:30   dinner Restaurant De Gelagkamer

Tuesday, November 2nd

09:30-10:30   Bruno Buchberger (invited speaker) Proving from first and intermediate principles [Mathematica notebook also readable with MathReader]
10:30   coffee
11:00-11:30   Giovanni Sambin Developing mathematics over type theory: tripartition of tasks [slides]
11:30-12:00   Georgi Jojgov A stepwise approach to formalizing mathematics [slides]
12:00   lunch
13:30-14:00   Randy Pollack Pragmatic reasoning about languages with binding? [slides]
14:00-14:30   Jasper Stein Gauss-elimination according to Coq [slides]
14:30   tea
15:00-15:30   Marc Bezem A depth-first implementation of geometric logic in Prolog [slides]
15:30-16:00   Loïc Pottier An experience: using Coq to do mathematics in the first year of university

The program of the workshop is still not finalized, and the second day might end later than in the current table.

Abstracts

Clemens Ballarin, Instantiation: Integrating Modules with Readable Proofs

Institut fuer Informatik, TU Muenchen

[slides]

The aim of modules in proofs is a higher level of abstraction. We discuss the integration of the Locale module system of Isabelle with Isar readable proofs through mapping Locale contexts to Isar contexts.

Marc Bezem, A depth-first implementation of geometric logic in Prolog

Institutt for Informatikk, University of Bergen

[slides]

Geometric logic (GL) is the logic preserved by geometric morphisms between topoi. The first-order fragment of GL extends resolution logic in that geometric clauses can have existentially quantified conclusions. A substantial number of reasoning problems (e.g., in confluence theory and projective geometry) can be formulated directly in GL without any skolemization. Thus no skolem axioms are necessary and the domain of discourse can be kept finite. These advantages can outweigh the disadvantage that a more expressive logic is generally more difficult to implement than a simpler one. We explore the balance between the advantages and disadvantages with an implementation in Prolog of (incomplete) proof search in GL including the generation of proof objects. If a proof has been obtained it can be verified directly in Coq. In this way proof objects have been generated for the induction steps in the proofs of the Hindley-Rosen Lemma and Newman's Lemma. These proof objects are relatively small and still readable.

Bruno Buchberger, Proving from first and intermediate principles

Research Institute for Symbolic Computation
Johannes Kepler University, Linz, Austria

[Mathematica notebook also readable with MathReader]

Building up provenly correct mathematical knowledge bases is a major challenge for the future of mathematics.

For this end, some (the majority of?) people pursue the approach of "first principles": Implement a simple proof checker for some version of (predicate) logic. The correctness of the proof checker is checked by inspection, which is deemed to be possible because it is so simple. If, in later stages of building up knowledge bases in special areas of mathematics, special proof generators are used, the resulting proofs are not yet considered as reliable but are considered only as proof proposals that have to be checked by the proof checker for obtaining the ultimate correctness certificate.

Alternatively, one can pursue an approach of "intermediate principles": Build up a hierarchy of simple / general and more sophisticated / special proof generators with the proviso that, for each proof generator, one has to give an (automated) correctness proof before the proofs generated are accepted.

In the talk, we will analyze and compare the two approaches and argue why we think that the approach of intermediate principles, in the long run, is more realistic.

Czeslaw Bylinski, Strengthening the Computational Power of the Mizar Checker

University of Bialystok

[slides]

Robert L. Constable, Foundations for the Management of Formal Mathematical Knowledge

Cornell University

[slides]

A small international community is gaining experience in managing formal mathematical knowledge, the sort arising from the use of theorem provers. At Cornell we have been involved in this activity for several years, stimulated by our use of three theorem proving systems, Nuprl, MetaPRL, and JProver and by Doug Howe's 1997 work combining results from Nuprl and HOL.

My lecture will highlight three of the discoveries we have made in this subject. One is about sharing content across logics and systems and is an extension of Howe's work by Evan Moran. Another is work by Stuart Allen on logical concepts that support proofs using results from different systems, hybrid proofs. The third are results from Lori Lorigo that help automate the organization of formal material for presentation and search. I will also discuss the future directions for our work.

Georgi Jojgov, A stepwise approach to formalizing mathematics

University of Eindhoven

[slides]

In this talk I present ongoing work on studying the process of creating a fully formalized and computer-checked document from a piece of informal mathematics. Our approach, based on Weak Type Theory (WTT), allows the definition of several stages of this process, each with increasingly stronger correctness requirements. Every one of these stages presents opportunities for computer assistance and checks that help the developer of the formal text and guarantees higher level of reliability of the formalization as a whole. I will discuss both the general setting and goals of the project as well as some recent ongoing work on the automatic translation of a segment of WTT into type theory with open terms.

Randy Pollack, Pragmatic reasoning about languages with binding?

Computer Science, Edinburgh University

[slides]

Based on old work (with James McKinna) on formalising the theory of PTS in LEGO, and recent work formalizing my TLCA'03 paper (with Thierry Coquand and Makoto Takeyama) in Coq, I'm interested again in the problem of reasoning about languages with binding. New papers about new approaches to this problem seem to appear every year. Do any of these approaches make it feasible to formalize your latest paper? What are the real difficulties, and where do each of the approaches fall down? Can mechanized tools remove some of the tedious details? An informal collaboration wants to develop a "challenge problem set" to help evaluate the various approaches. If you have encountered (or overcome) problems in this area, I want to hear about it.

Loïc Pottier, An experience: using Coq to do mathematics in the first year of university

INRIA Sophia Antipolis

Claudio Sacerdoti Coen, A Coq tactic for one step conditional rewriting

INRIA Futurs (Paris)

[slides]

We present a new Coq tactic that given an hypothesis H: E1 R E2 proves that (C E1) -> (C E2) provided that C is a composition of morphisms and possibly opening new goals of the form Ei Ri Ei. A morphism is a couple (f,∑) where f is a function of type T1 → ... → Tn → T and ∑ is a signature (T1,R1) →? ... →? (Tn,Rn) →? (T,R) such that ∀ x1 x'1:T1, x1 R?1 x'1 → .... → ∀ xn x'n:Tn, xn R?n x'n → (f x1 ... xn) R (f x'1 ... x'n) and R?i = Ri if →? is →+ (covariant argument) and R?i = Ri-1 if →? is →- (contravariant argument). If Ri is a symmetric relation than the i-th argument is both covariant and contravariant.

The tactic generalizes at once:

  1. setoid rewriting (when all the Rs are equivalence relations)
  2. partial setoid rewriting (when all the Rs are PER).
  3. one step reduction in rewriting systems (when the Rs are not requested to be symmetric; e.g. allows to beta-reduce a subterm in a lambda expression)
  4. inequality reasoning (e.g. to prove that -x2 * c * d < 0 provided that -x1 * c * d < 0 [original goal], x2 < x1 [hypothesis to rewrite] and (c > 0 and d > 0) \/ (c < 0 and d < 0) [new side conditions])

Giovanni Sambin, Developing mathematics over type theory: tripartition of tasks

Paulus Venetus Logic Group, University of Padua

[slides]

My principal claim, and proposal, is that the task of formalizing mathematics in type theory, which is sometimes considered as a burden on computer scientists, is actually better accomplished if it is organized as three strictly connected but distinct tasks, of mathematicians, logicians and computer scientists: developing (a new kind of) mathematics over a toolbox, devising a suitable toolbox or higher level notation, implementing the toolbox, respectively. The connections between the different "professions" should be seen as collaborative and dynamical in both directions. The convenient common language, or foundation, is a minimal type theory, which is compatible both with powersets and with the axiom of choice and which allows for modularity. I will illustrate my claims with general considerations and with some relevant examples taken from the development of formal topology and the basic picture.

Jasper Stein, Gauss-elimination according to Coq

Radboud University Nijmegen

[slides]

Gauss-elimination: the process of solving systems of linear equations by means of "sweeping" associated matrices. Based on my linear algebra contribution, I embarked on the formalisation of systems of linear equations, their associated matrices, elementary operations on them, and showing that the process of Gauss-elimination preserves the solution set of systems of equations. This is still work in progress.

Christian Urban, Nominal Techniques as an Isabelle/HOL-Theory

University of München

[slides]

I will describe how standard (informal) proofs about the lambda-calculus can be formalised with ease in Isabelle/HOL using a variant of Pitts' nominal approach to binders. First, an inductive definition for alpha-equated lambda-terms is given and then it is shown how a strong induction principle can be derived, which looks very much like the Barendregt variable convention.

Freek Wiedijk, Integrating procedural and declarative proof

Radboud University Nijmegen

[slides]

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.

Anna Zalewska, Mizar Mathematical Library in Education

University of Bialystok

[slides]

Roland Zumkeller, Towards a formal proof of the Kepler conjecture

PhD student in the project LogiCal, INRIA / laboratoire d'informatique de l'X (Ecole Polytechnique, Paris)

[slides]

In 1611 Johannes Kepler stated that the maximal density of a packing of spheres having the same radius is pi/sqrt(18). This value is in fact achieved by arranging the spheres in a rather intuitive way, as usually done by fruit sellers. Proving this conjecture remained a challenge for several centuries - some "proofs" were given, but they turned out to be erroneous. In 1998 Thomas C. Hales published a proof, which is not only very large, but makes also extensive use of computer programs (similarly to the proof of the four colour theorem). The complexity of these calculations leaves some uncertainty about their correctness, which has lead Hales himself to call for a formalization of his proof. My talk will focus on one type of problem which reoccurs throughout the proof: the formal verification of inequalities in real numbers. A global optimization method used in conjunction with a branch-and-bound algorithm are presented together with their correctness proofs in Coq.

Organisers

Herman Geuvers Nicole Messink Bas Spitters Dan Synek Freek Wiedijk

 

Getting to Nijmegen

Most of you will be arriving at Amsterdam Schiphol airport. The easiest way to get to Nijmegen from there is by train. The train station is under the airport (follow the train signs). Take a train to Duivendrecht (so not to Amsterdam Central Station) and change trains here (go one level up) to go in the direction Utrecht. From Duivendrecht there are direct trains to Nijmegen (via Arnhem). You may also take a train to Utrecht and change trains to Nijmegen there.

Especially on Duivendrecht station and on the trains from Schiphol to Duivendrecht be aware of pick-pockets. Keep an eye on your luggage at all times!

The train trip is 1 hour and 30 - 45 minutes. A typical trip is the following:

17:10  Schiphol (platform 1, direction Hilversum)
17:23 Duivendrecht
change train
17:29 Duivendrecht (platform 8, direction Utrecht CS)
18:41 Nijmegen

There is a train planner on the web (English version).

Hotels

We have good experiences with:

Hotel Apollo
Bisschop Hamerstraat 14
6511 NB Nijmegen
Tel.: +31 (0)24 - 323 35 94
Fax: +31 (0)24 - 323 31 76

A single room in Hotel Apollo costs 69 euro, including breakfast.

Slightly more expensive (the invited speakers will stay here) is:

Hotel Courage
Waalkade 108-112
6511 XR Nijmegen
Tel.: +31 (0)24 - 360 49 70
Fax: +31 (0)24 - 360 71 77

A single room in Hotel Courage costs 98 or 108 euro, including breakfast.

There also is a web page (although it is a few years old) with alternative accomodation.

Getting to Hotel Apollo

Hotel Apollo is very close to central station (400 meter). It is located in the Bisschop Hamerstraat, a very short street next to the Keizer Karelplein:

[map hotel Apollo]

The location of the central station is labeled with a blue cross.
The location of Hotel Apollo is labeled with a red cross.
The location of Hotel Courage is labeled with a green cross.
The location of Restaurant De Gelagkamer is labeled with a blue circle.

The Restaurant

The workshop dinner will be held at:

Restaurant De Gelagkamer
Waalkade 50a
6511 XP Nijmegen
Tel.: +31 (0)24 - 360 33 80

See the map above for the location of this restaurant.

Getting to the Workshop

The workshop will be held at the campus of the Radboud University.

To get to the campus by public transport take the train from Nijmegen station to Nijmegen Heyendaal. This train leaves from platform 35, and runs every 11 and 34 minutes past the hour. The train trip will take 3 minutes. From the train station the walk to the workshop locations takes another ten minutes.

There are also bus lines going to the campus. The buses that run through the Heyendaalseweg are lines 1 (direction Molenhoek) and 11 (direction Brakkenstein).

Here is a map of the campus:

[map campus]

The location of the station Nijmegen Heyendaal is labeled with a blue cross.
The location of the workshop on the first day (the "Gymnasion") is labeled with a red cross. Please note that the Gymnasion also contains a sports center, so it does not look very much like a university building.
The location of the workshop on the second day (the "Magnetenlab") is labeled with a green circle.
Bus stops are on this map indicated as little black ovals with a white "B" in it.

 

page maintained by Freek
picture from Jutting's formalization of Landau's Grundlagen (a fragment of the Peano axioms)