Programming Language Semantics and Program Logics: Twin-3

Funding Body: CEC Science

The Edinburgh Team

GRANT HOLDERS:
Professor Gordon Plotkin, Professor Eugenio Moggi

Other teams

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