ARPA: Advancing the Real use of Proof Assistants

Research project funded by the Netherlands Organisation for Scientific Research (NWO) under FOCUS/BRICKS grant number 642.000.501

Research

Proof Assistants are computer tools that help the user in developing a theory (stating definitions and lemmas), modelling systems (describing constructions, giving definitions) and verifying properties about these systems (giving proofs). So, Proof Assistants are very generic tools to support Formal Methods, the field of computer science that aims at describing, modelling and verifying systems using methods derived from logic and mathematics. Their genericity makes them less efficient than tools that are especially geared towards a specific formal method. On the other hand they have a very precise semantics, which makes the certainty of a result that is verified by a Proof Assistant very high. This is especially the case for PAs that are able to produce proof objects that can be checked independently. In the future, the very high level of certainty will prevail. In this project we want to advance the use of PAs in several ways:
  1. by developing a mathematical input mode for PAs, making theme more easy to use,
  2. integration of different PAs, allowing the exchange of results,
  3. further developing a certified library for real number computation in Coq,
  4. verifying hybrid systems in Coq, using the library of (3) to model and verify system properties.
The quality of (3) will be judged by its applicability to (4), but (2) and (3) will also be judged by their applicability to the formalisation of the proof of a large mathematical theorem, e.g. Hales' proof of Kepler's conjecture, which is presently being formalised in the Flyspeck project.

Research team

The ARPA research is carried out within the Foundations group and the ITA group (notably part 4 of the project mentioned above) of the Institute for Computing and Information Science (ICIS)of the Radboud University Nijmegen (NL).
The research team consists of researchers funded from the project and other people whose research falls within the scope of ARPA.

Context

ARPA is a BRICKS project, funded by NWO and BRICKS. The project runs from 1/9/2005 until 1/9/2009.

Talks, Publications, Software

Links

herman
Last modified: Thu Nov 2 22:44:30 CET 2006