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''.