Programming Language Semantics and Program Logics: Twin-3
Funding Body: CEC Science
- Grant value 59,500 pounds
The Edinburgh Team
- GRANT HOLDERS:
- Professor Gordon Plotkin, Professor Eugenio Moggi
Other teams
- University of Cambridge
- Universita degli Studi di Genova
Summary
The ultimate goal of much research in computer science is to make
feasible the use of formal methods in software development and
verification. An essential prerequisite for achieving such a goal is
to have program logics that can manage the variety and complexity of
real programming languages. The proposed project focuses on two key
issues regarding program logics:
- uniform presentation of programming languages and program logics, so that it will be easier to represent them in a logical framework for computer-aided reasoning;
- modular approach to programming languages and program logics, so that one can manage a wide range of programming languages and corresponding program logics by a few reusable modules.
We expect to achieve these objectives by a close cooperation among the
three sites involved, and by building upon recent work of the three
responsible scientists. We expect fruitful interaction with two
ESPRIT BRAs, ``Logical Frameworks'' and ``Categorical Logic in
Computer Science'', and two UK SERC projects, ``Logical and Semantical
Frameworks'', and ``Verifying ML programs using Evaluation Logic''.