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