Basic Research Action: TYPES
ESPRIT Basic Research Action 6453
TYPES: Types for Proofs and Programs
The TYPES project ran from 1 September 1992 until 30 October 1995. It is now running as the Esprit working group 21900 - TYPES, a working group in the ESPRIT program of the European Union.
The aim of the TYPES action is to develop proof assistant systems with applications both to the formalization of large pieces of mathematics and to proofs of correctness for software and hardware systems. This latter application is of increasing interest for the needs of the software and hardware industry.
However, the project is not only concerned with implementation but also with longer-term research, namely investigations in proof theory and logical formalisms applied to computer science, software engineering (including rewriting, unification, design of user interfaces, design of specification languages) and experiments in industrial applications (especially in cooperation with our partner Philips). Each of these fields of activity gives rise to possible improvements and new research questions in the other areas.
(This description is taken from an EATCS paper by Hugo Herbelin which describes the BRA. The paper is available in gzipped dvi (21K) format.)
This page contains links to the following:
- Proceedings resulting from the BRA.
- Sites involved in the BRA.
- Implementations which have come out of the BRA.
- A local page for the Edinburgh site.
Last updated on 11 February 1997 by Healfdene Goguen <hhg@dcs.ed.ac.uk>.