Dependently-typed tactics and certificate checking in Meta Dedukti
A transfer tactic for Meta Dedukti
A parser for Dedukti first-order problems as produced by FoCaLiZe that can pretty-print the problems in other formats.
Rec to Dedukti translator
Decision procedure for SL used in specification of memory allocators
Coq encoding of Natural Deduction, flavour of Predicate Calculus, up to completeness theorem
Prototype implementation of a mini-ML language with polymorphic variants and pattern matching using set-theoretic types.
Cours de Coq au M2 LMFI (partie 1 programmation fonctionnelle + partie 2 preuves formelles)