Organised in Cambridge by Mike Gordon and Tobias Nipkow, 24-25 Aug., 2009

Google Groups
Subscribe to ITPworkshop
Visit this group
Post comments by sending email to:
Subscribe to the group and then upload interesting papers.


It is hoped to produce a white paper reflecting the results of the workshop (e.g. future needs, ideas for actions, collaborations). The material below, which is expected to evolve, is derived from detailed notes taken at the workshop by Matt Kaufmann, together with comments that have been received. It is possible that some participants may feel that topics have been incorrectly emphasised, mentioned material is of low interest and important ideas have been omitted. Please send Mike Gordon input so that further versions can better reflect your views.

Integrated platforms

There is a striking agreement by almost everyone that interactive theorem provers should become integrated design, execution and verification platforms, with links to external tools. All the major ITP systems (ACL2, Coq, Isabelle, HOL, PVS) already support this and future plans emphasise the need for more research towards improving the integration. External facilities that can (and are) being linked include SAT and SMT solvers, proof search engines, model checkers, tools for numerical methods and computer algebra systems. There is also agreement that, if possible, external tools should provide proof certificates that can be replayed or otherwise checked by the importing ITP system.

It is especially remarkable that the major existing tools share a common vision, because they are based on widely different software architectures (e.g. extensible small kernel versus large pre-built tool suite) and logical foundations (classical set theory versus constructive type theory). Furthermore, they were developed within largely disjoint technical cultures.

Embedded computation

Embedded computation is not only useful for executing formal specifications; it is required for proofs needing lemmas proved by calculation (e.g. in the Four-Colour proof). A key component is having a programming language as part of the term structure of the logic supported by the theorem prover. Besides being used for computations within proofs, executable terms are also used for checking examples and counterexamples and for producing certified artifacts (e.g. trustworthy data). All major current ITP tools support computation to some extent, though they have quite different methods of executing programs and moving between computation and deduction.

Diverse uses of ITP

ITP systems have a diverse variety of uses that range from computer system verification to artificial intelligence. Examples include: assisting the creation and checking of mathematical proofs, design, verification and optimisation of hardware and software, formal synthesis of implementations from specifications, checking properties, finding errors and counterexamples, planning and constraint solving.

Although full proof of correctness is often seen as the ultimate goal of ITP applied to verification, simpler specification consistency checking can have great value (e.g. type checking, shape analysis, model checking, termination analysis etc). Experiments in seamlessly linking these to theorem proving have been done, but further work is needed, especially large case studies.

Interacting with theorem provers

There are a number of new ways of interacting with theorem provers in progress or being planned. These derive both from the way computing is evolving (e.g. availability of efficient parallel execution thanks to multi-core processors) and from the growing size of applications, particularly checking huge mathematics proofs. However, the research challenges of improving interaction may be tool and application specific and may be orthogonal to ITP and logical issues. There is some support for the idea of adopting modern software engineering methods for managing large proofs, both system architecture ideas and existing software development platforms (e.g. IDEs like Visual Studio, Eclipse, NetBeans).

It is not clear, however, if off-the-shelf software development interaction paradigms can be adapted for proof development. Interactive proof may need new kinds of interaction - some interesting ideas are already emerging. Hierarchical, graphical tools can help with organising, understanding and constructing large proofs. The Emacs-based Proof General front end is an existence proof that tool- and application-independent ITP interfaces can be successful, though opinions on the value and long-term prospects for Emacs are divided.

The challenge of large mathematical proofs

Theorem proving has now reached a stage where it is possible to perform (or attempt to perform) interactive proofs of very complex existing mathematical results such as Goedel's Theorems, the Four-Colour Theorem, the Kepler Conjecture (the Flyspeck project) and the classification of finite simple groups. This application area is putting demands on ITP tools to become more friendly to mathematicians. Although this work is "blue sky" research, it may open up new verification possibilities in software areas underpinned by sophisticated mathematical theories (e.g. cryptography). Challenge goals are: (i) having all of college mathematics formalised and available off-the-shelf for use by theorem provers (an estimate of 140 person years was given); (ii) automating high school mathematics using a combination of artificial intelligence and decision procedures. If progress is made on these challenges there may be applications to education (both generating course material and providing better computer support for teaching and grading students).

The duality of proving and refuting

The interaction needed to find proofs is seen as a positive creative process and not as a necessary evil. Support for prototyping proofs, like automatic generation of finite counter-examples and complex type checking, are already useful. Exploring the duality between proving and refuting may be a good route to getting more effective proof finding interaction with tools. Currently only finite counter-examples are supported, but there are new ideas emerging that might lead to ways for automatically generating symbolic counterexamples in areas such as continuous mathematics. Methods for visualising counterexamples would also be useful. Since most programs and initial conjectures contain errors, there was a general consensus that counter-example finding deserves a higher priority than it has traditionally enjoyed.

New tools may engender new kinds of mathematics

There is the possibility that ITP tools could aid in the creation of new mathematics rather than just check old material. Perhaps some kinds of future mathematics may only be possible with computer support (by analogy with how computer algebra systems enable previously intractable physics and engineering symbolic calculations). However, the current logics supported by existing ITP tools are recognised as not being attractive to mathematicians, so it will be hard to recruit people from the mathematical community to use them. The pseudo-natural language of Mizar and the outsourcing of Flyspeck to cheap smart Vietnamese mathematicians are successful, but very different, methodologies for engaging mathematicians. Neither of these approaches are likely to work on a larger scale, especially as the wider mathematical community is thought to be both sceptical and poorly motivated towards computer tools.

Shared formats and standards

For ITP to support large formal specification and verification applications, real world specifications of, for example, accurate semantics of widely used programming languages, networking protocols or modern processor architectures need to be available. This is a major challenge. Formal specifications are developed in a variety of formalisms and currently it is hard to port these between systems, so one can become "locked in" to a particular tool. If one has a project needing to reuse specifications in the formalisms of different tools, then complete formality of translation may be impractical and various semi-formal pragmatic compromises may be necessary.

Current standards tend to be informal and (sometimes deliberately and beneficially) ambiguous. Standards based on formal specification methods could enhance the accuracy of models used for verification, and benefits to the wider assurance certification community can be envisioned, e.g. the possibility of reference specifications and implementations being verified compliant to standards. A stepping stone to standards supported by formal specifications would be a better understanding of the semantical relationships between the specification formalisms of different tools.

Semantically justified formal translations between theories may be too demanding, but even tools just for translating definitions (specifications) could be a useful. Translations would be aided by recognised standard formats for different kinds of specifications. Proposals were made for: (i) extending the SMT-LIB format towards the kind of logics used for ITP, (ii) interchanging theories between different ITP logics, and (iii) exchanging judgements between ITP and automatic tools via a "toolbus". Such standard formats would enable common repositories for specification, reference implementations etc. to be better supported. A major challenge would be to have a stardard representation for general mathematics. This is much discussed, but there are no concrete proposals accepted within the ITP community. Having reference examples and demonstrator case studies in a standard format and in the public domain would provide a poweful resource for students, researchers and evaluators.

Cloud theorem proving

The Internet and "cloud computing" provide new distributed possibilities for creating mechanised theories. An inspiration is the success of experiments in the mathematics community of collaborative problem solving (e.g. Polymath). Could projects be run like Polymath to accelerate the development of formal theory infrastructure and also to stress existing tools? A clear challenge is how to fit together contributions built using different theorem proving software. Perhaps this could be seen as an add-on to QPQ or linked to the vdash concept.

Although the source code of all the major ITP tools is in the public domain, the degree to which the software is a traditional 'open source' development varies. More collaboration between different ITP communities is advocated as a way to boost progress, and optimistic signs are emerging.

Workshop presentations

Morning of Monday 24 August
    Freek Wiedijk           Three wishes
    Alan Bundy              A Hiproof Interface for Viewing and Constructing Proofs
    Joe Hurd                Theory Engineering: Proving in the Large
    Andy Gordon             Some Challenges for Future ITP
Afternoon of Monday 24 August
   Mechanising mathematics: scientific challenge and potential applications
    Laurent Théry           Formalising Mathematics
    Cameron Freer           Mechanised Mathematics: Four Provocations
    Rob Arthan
    John Harrison           Grumpy Old Man
Morning of Tuesday 25 August
   Search for bugs and search for proofs (discussion lead by Tony Hoare)
    Daniel Kroening         SMT-LIB for HOL
   Interfacing ITP to other tools and the real world 
    Daniel Kroening         Interfacing ITP to the Real World
    Peter Sewell            Interfacing ITP to other tools and the real world
    Tobias Nipkow 
    Shankar                 Interaction and Automation
Afternoon of Tuesday 25 August
   Konrad Slind             ITP Uses and Challenges at Rockwell Collins 
   Future dreams for current tools:
    J Moore, Matt Kaufmann  ACL2      
    Bruno Barras            Coq
    John Harrison           HOL Light
    Makarius Wenzel         Isabelle  
    Shankar                 PVS

List of participants

 Mark Adams                 (mark AT
 Mihhail Aizatulin          (avatar AT
 Rob Arthan                 (rda AT
 Bruno Barras               (bruno.barras AT
 Nick Benton                (nick AT
 Alan Bundy                 (bundy AT
 Cameron Freer              (freer AT
 Mohan Ganesalingam         (mg262 AT
 Georges Gonthier           (gonthier AT
 Andy Gordon                (adg AT
 Mike Gordon                (Mike.Gordon AT
 David Greaves              (David.Greaves AT
 John Harrison              (johnh AT
 Tony Hoare                 (thoare AT
 Peter Homeier              (palantir AT
 Joe Hurd                   (joe AT
 Paul Jackson               (Paul.Jackson AT
 Cliff Jones                (cliff.jones AT
 Matt Kaufmann              (kaufmann AT
 Andrew Kennedy             (akenn AT
 Daniel Kroening            (kroening AT
 J Strother Moore           (Moore AT
 Magnus Myreen              (Magnus.Myreen AT
 Tobias Nipkow              (nipkow AT
 Scott Owens                (Scott.Owens AT
 Matthew Parkinson          (Matthew.Parkinson AT
 Larry Paulson              (Larry.Paulson AT
 Andy Pitts                 (Andrew.Pitts AT
 Claudio Russo              (crusso AT
 Peter Sewell               (Peter.Sewell AT
 Konrad Slind               (klslind AT
 Natarajan Shankar          (shankar AT
 Georg Struth               (g.struth AT
 Laurent Théry              (Laurent.Thery AT
 Thomas Tuerk               (Thomas.Tuerk AT
 Viktor Vafeiadis           (viktorva AT mic
 Tjark Weber                (tw333 AT
 Makarius Wenzel            (wenzelm AT
 Freek Wiedijk              (freek AT
Please email Mike Gordon if there are any errors, or if you attended, but are not listed above and would like your name added.


Maintained by Mike Gordon.
This page last updated on September 15, 2009.