Edinburgh Site Page for the APPSEM Working Group

Esprit Working Group 26142 - Applied Semantics

electronic proceedings Workshop program abstracts of the talks dvi ps

Edinburgh is a site in the APPSEM working group.

TCOOL is a project in Edinburgh whith goals fitting in the general aim of APPSEM

The themes of APPSEM focus on the following general areas:

• description of existing programming language features (for example object oriented);
• design of new programming language features;
• implementation and analysis of programming languages;
• transformation and generation of programs;
• verification of programs.

The themes are

• A: Semantics for object-oriented programming
• B: Program structuring
• C: Integration of functional languages and proof assistants
• D: Verification methods
• E: Automatic program transformation
• F: Games, sequentiality, and abstract machines
• G: Types and type inference in programming
• H: Semantics-based optimisation
• I: Domain theory and real number computation

Edinburgh.

The research team at Edinburgh is part of the Laboratory for the Foundations of Computer Science (LFCS) within the Department of Computer Science. The site leader is Samson Abramsky.

The LFCS is one of the largest research groups in Foundations of Computer Science in Europe, with about 70 members. There is extensive expertise in type theory (Plotkin), computer-assisted formal reasoning (Burstall), formal specification and program development (Sanella), semantics of programming languages (Plotkin, Abramsky), concurrency (Stirling, Bradfield, Abramsky), axiomatic and synthetic domain theory (Plotkin, Fiore, Simpson) and the applications of category theory to Computer Science (Plotkin, Power). Systems developed at LFCS include Standard ML, Lego, and the Concurrency Workbench.

Edinburgh expects to contribute to themes A, D, G and H.

TCOOL Typed Concurrent Object-Oriented Languages: foundations, methods and tools.

This is a joint project between the Department of Computing, Imperial College, London and the Department of Computer Science, University of Edinburgh. We also have a collaborator at the Computing Laboratory, Oxford University. The project is funded by EPSRC.

The aim of this project is to provide sound semantic foundations for languages such as Java, and to develop methods and tools for the analysis and certification of programs written in these languages.

The goal is towards obtaining a mapping of Java (or any similar language with concurrent object-oriented features) into a small core calculus, which is a typed lambda-calculus plus non-determinism and state. This mapping is important for us in the light of our recent work using game semantics to give fully abstract models for Idealized Algol and a number of other languages. For program analysis and verification, it is intended to apply static analysis techniques based on abstract interpretation.

PARTICIPANTS

Imperial College

• Chris Hankin
• Russ Harmer
• Pasquale Malacaria
• Rajagopal Nagarajan
• Prahladavaradan Sampath

University of Edinburgh

• Samson Abramsky
• Juliusz Chroboczek
• Jim Laird
• Martin Wehr

Oxford University

• Guy McCusker

Last modified: Mon Feb 7 12:55:02 GMT 2000