Main page

Objectives and state of art

Research groups

Software

Tutorials and advanced lectures

The Types mailing list

Previous events

Organisation

Contact

Manchester

The Manchester site is the Formal Methods and Mathematical Foundations groups, in the Manchester University Computer Science Department. It has participated in all previous EU funded TYPES working groups. The site has considerable expertise in mathematical logic, category theory, automated deduction and machine checked mathematics. Current interests of the site include proof assistants for mathematicians and mathematics education, logical frameworks, constructive set theory and constructive topology.

The site will mainly contribute to the objectives of Formal Mathematics and Mathematics Education and Foundational Research.

• Manchester has a UK/EPSRC funded project (Pythagoras), jointly with the Durham site of this proposal, to work widely on aspects of Formal Mathematics and Mathematics Education
• Peter Aczel and others will continue to work on constructive set theory and its relationship with dependent type theory. In particular their work on constructive topology (in constructive set theory) will be developed in parallel with the work on formal topology (in type theory) of the Padua subsite. There is also a planned workshop on Formal Topology in the current proposal.
• Work on logical frameworks, arising from Robin Adams' PhD work will continue.

The senior members group relevent to our proposal, are

• Peter Aczel (contact person)
• David Rydeheard
• Andrea Schalk
• Andrei Voronkov

The site has regularly taken part in the previous TYPES annual meetings, small workshops and site visits. The site has particularly close collaboration with the Durham site, including joint UK-funding, and many visits by researchers and students.

Manchester homepage