Interactive Proof Assistents

(Thursdays, 14.00-16.00, room 140)

Although it is called seminar, it will not be a seminar in the usual sense. The goal is that we get acquainted with systems for formal proof verification mostly by practicing. We will probably read some papers as well, but the emphasis is on practice.

Schedule

Mizar

For Mizar, I found the following texts very useful: An Outline of PC Mizar , by Michal Muzalewski. Mizar: An impression by Freek Wiedijk, and Mizar in 9 easy steps , probably by Piotr Rudnicki. I propose that we verify the following text in Mizar, about differences and summations.

(Below you can read the original schedule of the seminar, which was extremely optimistic)

The first half (say 6 lectures) will be used for getting acquainted with the system and with the underlying logical principles. I will introduce some theory, (inductive data types, recursion, some lambda calculus and higher-order logic) and we try to make some small formalizations in the selected systems. For example, we introduce the natural numbers, addition, multiplication, and we try to prove some standard properties of those, like commutativity, associativity, and distributivity.

For the second half of the seminar, each student should choose a bigger verification project and a system in which he wants to carry out this project. The projects can also be made in groups (of say 2 persons) Possible projects are:

You can choose another project as well. I intend to use the following systems. If you want, other systems can be also considered.

HOL-light

HOL stands for Higher-Order Logic. (See the homepage of the system ) HOL is an abbreviation for Higher-Order Logic. It is well-documented and it offers a reasonable level of automation. Proofs can be constructed interactively. It is called light because it is derived from an earlier system, developed by Mike Gordon, which apparently was more complicated. HOL-light is developed by John Harrison.

Mizar

Mizar is a Polish construction. It is called after a star in Ursa Major which is only 78 light years away. (When the light that you see now left the star, Ul. Joliot Curie was still called Uferstrasse. You will probably never see the arrival of the light that is departing now) The system was initiated by Andrzej Trybulec in Bialystok in 1973. (See here for the homepage of the system , see also here ) The best documentation seems to be here . Mizar is based on Grothendieck-Tarski set theory. My first impression from studying the documentation is that understanding this system is going to be quite a challenge, but some impressive formalizations have been made in it, so we should try. The system offers no support in constructing the proofs. It is a batch system. This means that the user has to type the proof in a text-editor. After that, Mizar reads the text and reports the errors.

Coq

The name probably derives from Thierry Coquand and coq (rooster), which is kind of a French national symbol. Another possibility is that it means 'calculus of constructions (qonstructions?)' The system implements intuitionistic higher-order logic through the Curry-Howard isomorphism. The level of automation is lower than HOL-light's, but higher than Mizar's. The system is well-documented and the developers are working hard to introduce more automation. The homepage is here . (We will probably not have time to do any projects in Coq. I will probably give only a short demonstration)