Previous | 
Home
Section: Software
Dedukti
Participants : Mathieu Boespflug [Contact] , Gilles Dowek.
Dedukti
is a universal proof checker, based on 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