Types for Proofs and Programs


TYPES - 6453

Work Area: Logics and Logic Programming

Keywords type theory, proof assistant, lambda calculus, unification


Start Date: 1 September 92 / Duration: 36 months / Status: running

[ participants / contact ]


Abstract TYPES is concerned with the automation of mathematical reasoning and its application to computer science. Formal proof will play a major role in future technology for the design of correct hardware and software. During LF, the Logical Frameworks action (3245), several proof systems were developed, all but one based on type theory, using the slogan "Propositions as Types". These systems will be enhanced and their use explored for developing some basic theories of mathematics and computer science. A main feature will be development of structured libraries of theories which will form a basis for experimental applications.


Aims

The aim of TYPES is to enhance the proof assistant systems ALF, Coq, Isabelle, Lego and PROPRE and produce libraries of theories in selected areas of mathematics and computer science. The structuring of these theories and questions of commonality for different proof systems will be topics for investigation, along with the foundations of proof systems, variants of type theory, and logical frameworks.

Approach and Methods

The Logical Frameworks of LF action (3245) developed four general proof assistants and a more specialised system (Propre). Three of the proof assistants are based on type theory, the fourth, Isabelle, uses the idea of logical frameworks, and has been used to implement types calculi. The type theory systems use the "Propositions as Types" paradigm in the form of Martin-Löf Type Theory (ALF) or Calculus of Constructions (Coq, Lego). The design of such systems raises both basic questions and pragmatic ones concerning algorithms and implementation: for example, how to define inductive data types, what unification algorithms to use, how to delay the binding of "logical variable", and what is a good form of user interface.

Given such a system, TYPES will build basic theories for mathematical systems such as natural numbers, integers and reals, and sets, as well as for theories of more interest to computer scientists such as lists, trees, regular expressions and finite state machines. The project will also consider the appication of such proof assistants to the formal validation of software.

The consortium also intends to try out tools on specific computer science applications such as protocol verification, and on mathematical applications such as analysis.

Potential

The development of these proof assistants and associated bodies of formalised and machine checked theories in mathematics and computer science will enable the tackling of problems involved in the correctness proofs for software and hardware systems. They will also provide specification languages with clear formal semantics and machine support.


Coordinator

INRIA Rocquencourt - F
Domaine de Volceau
B.P. 105
F - 78153 LE CHESNAY

Partners

Technische Universität München - D
INRIA Sophia Antipolis - F
CNRS - Université de Paris VII - F
Università di Torino - I
Nederlandse Philips Bedrijven - NL
Chalmers Tekniska Hogskola - S
University of Edinburgh - UK
University of Cambridge - UK
University of Manchester - UK

Associate partner

Universiteit van Nijmegen - NL

CONTACT POINT

Gérard Huet
tel +33/1-39 63 54 60
fax +33/1-39 63 53 30
e-mail: Gerard.Huet@inria.fr


LTR synopses home page LTR work area index LTR acronym index LTR number index LTR Projects index
All synopses home page all acronyms index all numbers index

TYPES - 6453, August 1994


please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook