Theoretical Computer Science is broadly divided into disciplines dealing with logic, semantics and formal methods on the one hand, and algorithmics and computational complexity on the other. The programme will focus on active areas of research that cut across this divide, dealing with algorithmic and complexity aspects of logic as well as logical methods in complexity. Among the areas of focus are
Computer-Aided Verification: Specifically dealing with algorithms and structures for verifying properties of computing system and the logical, combinatorial and algebraic methods deployed in their study.
Finite Model Theory: This draws on logic and combinatorial methods to study the expressive power of logical languages in the finite. Along with connections with complexity, the programme will explore applications in database theory, constraint satisfaction, proof complexity and process logics.
Proof Complexity: At the interface of logic and complexity theory, the study of proof complexity, both in terms of lengths of proofs and complexity of inference steps, provides powerful methods for complexity lower bounds.
Constraint Satisfaction: This describes a class of combinatorial search problems that arise in a wide variety of areas of computer science and which have been the focus of sustained research drawing on a rich variety of techniques from algebra, logic and graph theory.
Games: While two-player games are used as a tool in many of the areas mentioned above, an emerging theory combines games with automata and logic into a powerful tool for the analysis of sytems. Fundamental questions concern the algorithmic complexity of determining a winner or constructing a winning strategy, given a game and a winning condition.