Current Funding

ANR Blanc "Confidence, Proofs, and Probabilities" (CPP)

ANR Blanc "Parallelism and Distribution Analysis" (Panda)

ANR Jeunes chercheuses "Proof-Search in Interaction with Domain-specific methods"(Lengrand)

INRIA ARC REDO: Redesigning Logical Syntax

ANR Blanc "Theory and Application of Deep Inference" (INFER)

Funding period: Jan 2007 - Dec 2009. Money for equipment, traveling, and hiring 2 postdocs and 1 PhD. 3 Sites: LIX, PPS, LORIA. People from LIX: Lutz Straßburger, Dale Miller, Alexis Saurin, David Baelde, Gilles Dowek; from PPS: Michel Parigot, Jean-Baptiste Joinet, Stéphane Lengrand, Séverine Maingaud; from LORIA: Fraçois Lamarche, Silvain Pogodalla, Philippe de Groote, Claude Kirchner, Guillaume Burel.

Slimmer

Slimmer stands for Sophisticated logic implementations for modeling and mechanical reasoning is an "Equipes Associées" with seed money from INRIA. This project is initially designed to bring together the Parsifal personnel and Gopalan Nadathur's Teyjus team at the University of Minnesota. We also hope to expand the scope of this project to include other French and non-French sites.

Completed funding

Mobius

Mobius stands for "Mobility, Ubiquity and Security" and is a Proposal for an Integrated Project in response to the call FP6-2004-IST-FETPI.

PAI Germaine De Stael "Deep Inference and the Essence of Proofs"

Funding period: Jan 2007 - Dec 2008. Money for traveling between Paris and Bern. People from Paris: Lutz Straßburger, Dale Miller, Alexis Saurin, David Baelde, Michel Parigot, Stéphane Lengrand, Séverine Maingaud. People from Bern: Kai Brünnler, Richard McKinley, Phiniki Stouppa.

PAI Amadeus "The Realm of Cut Elimination"

Funding period: Jan 2007 - Dec 2008. Money for traveling between Paris and Vienna. People from Paris: Lutz Straßburger, Dale Miller, Alexis Saurin, Michel Parigot, Séverine Maingaud. People from Vienna: Matthias Baaz, Agata Ciabattoni, Stefan Hetzl, George Metcalfe

Types

The current Types contract started September 2004. This European project is the continuation of a series of previous Types projects (dating back to 1992).

Vallauris

Vallauris is a PAI ("les programmes d'actions intégrées") within Programme Picasso 2005 of Égide. The Vallauris project's scientific title is Integrating Proof Theoretic techniques and Semantic Tools in Proof Carrying Code and Validation and Analysis of Declarative code.

Rossignol

Rossignol is an ACI-Securite that deals with the verification of cryptographic protocols.

GeoCal

GeoCal is an ACI-Nouvelles interfaces des mathematiques project. GeoCal collects together 10 research terms in logic, theoretical computer science, and algebraic topology.