Explore projects

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