Next: Sheffield
Up: Cooperating sites
Previous: Royal Holloway


The Logic team of the math laboratory within the Université de Savoie has participated in all the previous EU funded TYPES working groups as a subteam of Paris VII team.

We have worked with pure and typed lambda-calculus and C. Raffalli is the author of the PhoX proof assistant, a proof assistant which is very easy to learn (this is a design requirement of the system) and used for teaching math.

Current interests of the team include proof assistants, proof and extraction of programs using classical logic, process calculi, proof of normalisation of typed calculi.

The senior members of the Programming Logic Group are

We have deep contacts with the Paris VII team arround the implementation of PhoX.

C. Raffalli and R. David have a project with the INRIA Nancy and the linguistic team of Paris VII to develop an interface using natural languages for PhoX (this project is founded by an ACI).

C. Raffalli, R. David and P. Roziere work on the teaching application of PhoX.

C. Raffalli works an a process calculi with Curry Howard. R. David and K. Nour work on proof of strong normalisation for various classical proof system.

Savoie homepage

Bengt Nordström 2005-09-22