Next: Toulouse
Up: Cooperating sites
Previous: Tallinn


Torino

The senior members are

The group's research is focused on the study of (compile-time) techniques for program analysis, using essentially tools and techniques of constructive logics and type theory developed by the other sites of the Types projects.

The main goal is the development of systems for formal reasoning about programs and the study of their application to program transformation and optimization. Type inference systems for various kind of analysis (like useless-code, strictness, and totality) of higher-order functional programming languages have been developed and studied, and the research mainstream is now evolving toward languages with imperative and distributed features. Further perspectives are in the study of software validation and security.

A foundational interest of Torino group in the field of constructive logics is in the programming-with-proofs paradigm in the style of logical frameworks like Coq. The main concern is with methods to obtain actual programs out of formal proofs, both in intuitionistic and in classical logic.

As next step in our research, we plan to implement a prototype of a Useless-Code Elimination (UCE) for higher-order typed functional programs with let-polymorphism. The long-term goal is being able to optimize code extracted from proofs in the Coq system by the other sites of the project. Several related applications are expected from this work, for instance a typechecker for rank 2 Intersection Types for (a subset of) Caml, the language used in the implementation of Coq.

On the foundational side of type theory, we plan to develop a semantical constructive interpretation of non-recursive maps and Classical Arithmetic, relating the constructive content of classical proofs to parallel typed computations.

Torino homepage


Bengt Nordström 2005-09-22