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:
The themes are
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.
University of Edinburgh
Last modified: Mon Feb 7 12:55:02 GMT 2000