This group works on foundational connections between mathematics, logic and computation. This includes work on category theory, logic and type theory. Current topics include: categorical and logical foundations of higher-order abstract syntax; general categorical frameworks for programming language semantics; axiomatic domain theory; variations on logical relations; realizability models of computation; modelling computational features such as control, state and mobility; game semantics; and linear logic. This work is now sufficiently mature that it is possible to provide accurate and concise semantic models of many features of full-scale programming languages. In the medium to long term this will have a significant impact on implementations and reasoning tools for such languages. Particular achievements include seminal work in axiomatic domain theory, foundations of higher-order abstract syntax, the theory of logical relations, game semantics and full completeness results in linear logic. Work on highly expressive type theories has formed the basis for a very influential range of proof assistants including Lego and Proof General (a generic interface for proof assistants). These systems are in wide use and have been applied to verification tasks in real systems e.g. in distributed garbage collection and verification of reactive systems. It is not much of an exaggeration of the international impact of this group to say that LFCS leads in this area and the rest of the world follows. Recently Simpson has been awarded an EPSRC Advanced Research Fellowship to study axiomatic accounts of the semantics of computation.
| Samson Abramsky |
|
Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk Please contact our webadmin with any comments or corrections. Logging and Cookies Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh |