Main page

Objectives and state of art

Research groups

Software

Tutorials and advanced lectures

The Types mailing list

Previous events

Organisation

Contact

Helsinki

The group in Helsinki is known for its work on the application of type theory to natural language (Aarne Ranta, now at Göteborg) and to constructive geometry (Jan von Plato). Both applications have led to extensive subsequent work in several sites of the Types group, including computer implementation with different proof editors.

The group will mainly contribute to the project objective Foundational Research. The group is interested in the application of methods from proof theory to decision problems in formalized mathematics. This includes lattice theory and elementary geometry, and the decision problem of intuitionistic modal logic - a problem that had resisted attempts at a solution for several decades but now seems to be solved. This last topic is of considerable interest for computer science applications of logic.

The senior members are:

• Jan von Plato, contact person
• Petri Mäenpää, Nokia
• Sara Negri

The area in which most collaboration is expected is in the development of proof systems for constructive geometry on which at least two other sites have worked or are presently working (INRIA Sophia-Antipolis, Nancy). The earlier collaboration with Göteborg (Aarne Ranta on the proof editor PESCA and Thierry Coquand on the proof theory of order relations) is planned to be continued.

Helsinki homepage