Funding

Current Funding

• ERC Advanced Grant “ProofCert: Broad Spectrum Proof Certificates” awarded to Dale Miller for  the five years 2012-2016.  A technical description is available.
• INRIA Equipe Associée Recent Advances in Proof Theory for Logical Specifications (RAPT). See also the official INRIA page
• INRIA ARC Eternal on Interactive Resource Analysis (2011-2012)
• ANR-FWF Blanc “Structural and Computational Proof Theory” (STRUCTURAL)

Completed funding

• ANR Blanc “Confidence, Proofs, and Probabilities” (CPP)
• ANR Blanc “Parallelism and Distribution Analysis” (Panda)
• ANR Jeunes chercheurs/ses “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: Franç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ée” 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.
• 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.