# 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:
- by developing a
*mathematical input mode* for PAs, making theme more easy to use,
- integration of different PAs, allowing the exchange of results,
- further developing a certified library for real number computation in Coq,
- 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