FORMES seminar
Hugo Herbelin is the head of the Coq development effort at INRIA.

Abstract: Coq is a based on a formalism, the Calculus of Inductive
Constructions (CIC), which is both a logic and a programming language. As a
logic, it is an expressive system of a strength comparable to set theory while
as a programming language, it is a strongly typed purely functional language
whose rich (dependent) types can express arbitrary specifications.

After a survey of some current issues with the development of Coq, we will
focus on the typing rule of the construction of pattern-matching on objects of
algebraic data-types. Following ideas coming from the Agda proof assistant, we
will discuss how to automatically infer a decidable subset of directly usable
typing constraints so as to lighten the writing of programs in the CIC.