Coq implementation and verification of a decision procedure for intuitionistic tautological properties (MPRI 2.7.2 project).
