Up: Cooperating sites
Previous: Dassault Aviation
Edinburgh
The Laboratory for Foundations of Computer Science (LFCS) in the School of Informatics of Edinburgh University, has participated in all four previous EU funded TYPES projects. LFCS workers developed the LEGO proof tool and the Proof General user interface, both widely used by researchers at other TYPES sites. LFCS researchers also contributed much to the theoretical basis on which all TYPES work rests, including topics such as logical frameworks, abstract syntax and variable binding, inductive definitions, consistency proofs and extensionality. This work is represented by many talks at TYPES workshops and publications in TYPES proceedings and other international refereed forums, often in collaboration with workers from other TYPES sites.
The site plans to contribute mainly to three project objectives.
- In proof technology, the future direction for the Proof General generic user interface for proof tools,1 laid out in a white paper, is to re-engineer and expand the system, centering around a well-specified protocol for interactive proof to be implemented by message passing in XML.
- In foundational research, it is planned to continue the collaboration with the Chalmers site on semantics and implementation of logical frameworks with subtyping and modules.
- On correctness of computer systems, Edinburgh has strong collaboration with the Durham and Nottingham sites on programming with dependent types. We are discussing collaboration on this topic with other sites. Also Edinburgh has collaboration with LMU Munich on mobile resource guarantees, proof-carrying code where the proofs guarantee the code will adhere to a resource specification.
The senior members are
- Robert Pollack, contact person
- David Aspinall
- Jacques Fleuriot
- Paul Jackson
- Gordon Plotkin
Bengt Nordström 2005-09-22