Objectives of the project and the state of the art
Europe needs robust software systems. Society has become dependent on computer systems working in an expected way, but programs are often erroneous. Like all big problems the software crisis can only be solved using a multitude of approaches.
We believe that one such approach is to use the computer to develop provably correct computer systems. Our contribution to this approach spans from fundamental research in logic to concrete formal proofs of major importance. This is an area where Europe has built up considerable competence during the last two decades within the TYPES community.
Research associated with previous EU funding for TYPES has led to logics based on various type theories (e.g. Extended Calculus of Constructions, Calculus of Inductive Constructions), proof tools based on these logics (implemented proof assistants such as Coq, LEGO, Alfa, Isabelle and Mizar), and mathematics libraries which are essential for practical use of the proof tools (e.g. the Mizar mathematical library, the Isabelle developments of set theory and higher-order logic, and the Constructive Coq Repository at Nijmegen). Some of this work is mature, widely used, and proven in significant examples and applications.
Computer assisted formal reasoning is also important for the development of mathematics. Our proof tools have been used to develop machine checked proofs of significant mathematical results. We want to use our work to develop systems that will be useful to mathematicians and other scientists in their proof-oriented work, much as computer algebra systems have been useful for symbolic computations. The preparation and checking of mathematical documents will gain convenience and reliability from machine support. Large libraries of mathematical knowledge can be made available for fast searching with machine support. Proofs from libraries can be studied at greater or lesser levels of detail. Such libraries can support cooperative and distributed working on extended projects. These facilities will also be useful in mathematics education.
Our plan to progress on these issues has the following four parts:
- Correctness of Computer Systems: tools and techniques aimed specifically at application of formal methods to system correctness, e.g. programming language specific tools and problem-specific automation of proof search.
- Formal Mathematics and Mathematics Education: this is the prototype example for proof in the large, including very high level mathematical vernacular languages, the construction and use of necessarily large libraries of previous work, and distributed working on long-term projects.
- Proof Technology: the details of proof, including unification, resolution, rewriting, general proof search, tactic languages and declarative proof languages.
- Foundational Research: underlying the previous three areas must be research on the expressiveness and relative correctness of the foundational logics, including syntax, semantics, definitional mechanisms, allowed computation and subtyping.
These ideas must be implemented; practical improvement of our working systems is an important part of our objectives. This includes further development of proof assistants, user interfaces and interfaces between tools so they become capable of supporting realistic scale work in many areas.