TYPICAL - 2011 - Annual activity report

TYPICAL

TYPICAL - 2011

Project Team Typical

Members

Overall Objectives

Presentation

Scientific Foundations

Logical formalisms
Libraries of formalized mathematics
Proof search and automated decision procedures

Application Domains

Certified decision procedures
Formalized mathematics

Software

Coq
Coqfinitgroup
Dedukti
Ssreflect

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

Regional Initiatives
National Initiatives
European Initiatives
International Initiatives

Dissemination

Organization of scientific events
Program chairs
Program committees
Participation to thesis committees
Reviews
Invited talks
Collective responsibilities
Popular Science
Teaching

Bibliography

Major publications
Publications of the year

Previous |

Home | Next next

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 $π r^{2}$ INRIA Paris-Rocquencourt project-team, and some members of the TypiCal team are active developers of the system.

Previous |

Home | Next next