Home

Collaborations

Contracts

  • Some members of the TypiCal project participate to the Mathematical Components project within the INRIA-Microsoft Research joint centre.
  • The ANR DeCert project aims at building trustworthy verification tools based on the collaboration of SMT-like decision tools and proof assistants.
  • The ANR PSI project aims at investigating how to take into account the specificities of a given theory when designing proof search methods, both in the theory of proof search and in the design of automated tools.
  • The European ForMath project from the EU FP7 STREP FET-open program proposes to develop libraries of formalized mathematics concerning algebra, linear algebra, real number computation, and algebraic topology.

Past Contracts

  • The INRIA ARC Corias, about the conception of proof assistants based on superdeduction modulo.
  • TYPES, a working group in the ESPRIT program of the European Union.

Teams

  • The PiR2 project at Inria Paris Rocquencourt explores the correspondence between programs and proofs as well as the metatheory and implementation of the Coq system, especially its features as dependently-typed programming language.
  • The ProVal project at Inria Saclay Île de France proposes methods and tools that can be integrated into the software development cycle and that make it possible to produce code that is proven to be correct with respect to its expected behavior.
  • The Parsifal project at Inria Saclay Île de France exploits recent developments in proof search and logic programming to make the specification of operational semantics more expressive and declarative and develops techniques and tools for reasoning directly on logic-based specifications.
  • The Marelle project at Inria Sophia-Antipolis Méditerrannée investigates formal methods to prove programs formally and develop libraries of formalized mathematics.
  • In Nancy, the Pareo project aims at designing and implementing tools for program specification and verification, incorporating constraint solving and term rewriting techniques.

International collaborations

  • The Foundations group in Nijmegen, the Netherlands, studies mathematical theories concerned with computability, provability and complexity.
  • The Psycotrip group at University de la Rioja, Spain, studies the design, specification and construction of symbolic computation systems for Algebraic Topology.
  • NIA is a research institute for the aerospace and atmospheric fields. It hosts a Formal Methods group working tightly with scientists at the NASA Langley Research Center.