Previous | 
Home
Section: Software
Coq
Participants : Bruno Barras [Contact] , Jean-Marc Notin, Arnaud Spiwack, Enrico Tassi.
Coq is a major proof
system an the primary object and / or tool of our research. Its
development is now mainly coordinated by the
Project
Team
Typical
Overall Objectives
Scientific Foundations
Application Domains
Software
New Results
- Semantics of the Calculus of Inductive Constructions
- Relative Strengths of set theory and type theory
- A Consistency model of Coq extended with decision procedures
- Towards a concurrent architecture for the Coq kernel
- Physics of computation
- Binders
- Interfacing Coq with SMT solvers
- SMT techniques for optimization problems
- Formal correctness of embedded programs
- Formal proofs for convex optimization problems
- Formal proof in real algebraic geometry
- Constructive mathematics
- Intersection types
- A simple presentation of the effective Topos
- A formal proof of the Feit-Thompson theorem
- A formal library for polynomial arithmetics
- Weak Memory Models
Partnerships and Cooperations
Dissemination
Bibliography
Project
Team
Typical
Overall Objectives
Scientific Foundations
Application Domains
Software
New Results
- Semantics of the Calculus of Inductive Constructions
- Relative Strengths of set theory and type theory
- A Consistency model of Coq extended with decision procedures
- Towards a concurrent architecture for the Coq kernel
- Physics of computation
- Binders
- Interfacing Coq with SMT solvers
- SMT techniques for optimization problems
- Formal correctness of embedded programs
- Formal proofs for convex optimization problems
- Formal proof in real algebraic geometry
- Constructive mathematics
- Intersection types
- A simple presentation of the effective Topos
- A formal proof of the Feit-Thompson theorem
- A formal library for polynomial arithmetics
- Weak Memory Models
Partnerships and Cooperations
Dissemination
Bibliography