Main page

Objectives and state of art

Research groups

Software

Tutorials and advanced lectures

The Types mailing list

Previous events

Organisation

Contact

Birmingham

The Birmingham group is in the Computer Science Department of the University of Birmingham. The group is working on both foundational and practical aspects, including work on semantics for proof search, program verification using linear logic to model state change, probabilistic model checking, automated verification for distributed systems, and representations for mathematics. Research in the group is supported by EPSRC, ESPRIT and the Midlands e-Science Centre.

The main contributions of the group to the objectives will be:

• Correctness of Computer Systems: to use linear logic to describe state change in object-oriented languages;
• Formal mathematics and mathematics education: to continue the work on representation for mathematics, developing an object-centred and hierarchical representation of concepts by frames that approximates mathematical practice;
• Proof technology: to work on automated verification techniques, including combining model checking and theorem proving;
• Foundational research: to work on a semantics describing control during proof search.

The senior members of the group are:

• Eike Ritter, contact person
• Achim Jung
• Manfred Kerber
• Marta Kwiatkowska
• Uday Reddy
• Mark Ryan

In the previous TYPES project, Ritter has visited Padova several times, in connection with the work on program verification. The group is also collaborating with Nottingham in teaching courses about type theory to starting PhD-students.

Birmingham homepage