Next: INRIA-Futurs
Up: Cooperating sites
Previous: Grenoble


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:

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

Bengt Nordström 2005-09-22