Categorical Logic in Computer Science II


CLICS II - 6811

Work Area: Logics and Logic Programming

Keywords category theory, logic, domain theory, linear logic, programming language semantics & logics, concurrency, type theory, constructive mathematics


Start Date: 1 October 92 / Duration: 36 months / Status: running

[ participants / contact ]


Abstract This project aims to apply the concepts and techniques of category theory and categorical logic to a number of key areas in computing science. These include: the study of type structures for programming languages; the development of structuring principles and axiomatic frameworks for semantics, as a basis for computational logics; and unified treatments of logics and models for parallel computation, and of specification formalisms. The work is based on the results of the CLICS action (3003).


Aims

CLICS II addresses the following key issues in the area of the unification of formalisms:

Approach and Methods

CLICS II aims to make decisive progress in four main areas: domain theory, semantics and logics of programming languages, concurrency and linear logic, and type theory and constructive mathematics. The cooperation between partners will be organised around a number of specialised workshops focusing on specific themes: sequentiality and stability, duality in domain theory, logic of inductive and recursive datatypes, subtypes and polymorphism in higher-order languages, higher order modal program logics, monadic programming language semantics, applied linear logic, computational content of classical logic, symbolic computation. Each theme addresses issues that span across several or all the main objectives of the project.

Potential

The new formalisms and logic systems which result from the project should contribute to future developments in high-level programming language design and in mechanised checking or derivation of proofs of correctness of computer systems. The main potential for exploitation will lie in the fundamental insights and methods made available for more applied work.


Coordinator

Imperial College of Science, Technology and Medicine - UK
180 Queen's Gate
UK - LONDON SW7 2BZ

Partners

Aarhus Universitet - DK
CAIMENS - F
Università di Genova - I
Chalmers University of Technology - S
University of Cambridge - UK
Associate parters
GMD - D
Technische Hochschule Darmstadt - D
University of Sussex - UK
University of Manchester - UK

CONTACT POINT

Prof. S. Abramsky
tel +44/71 589 5111
fax +44/71 581 8024
e-mail: sa@doc.ic.ac.uk


LTR synopses home page LTR work area index LTR acronym index LTR number index LTR Projects index
All synopses home page all acronyms index all numbers index

CLICS II - 6811, August 1994


please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook