Automated Certification of Implicit Induction Proofs. - Sorin Stratulat; Vincent Demange (CPP, 2011)

Vers un calcul des constructions pédagogique. (Toward a Pedagogical Calculus of Constructions). - Vincent Demange (2012)

Investigations on a Pedagogical Calculus of Constructions. - Loïc Colson; Vincent Demange (J. Univers. Comput. Sci., 2013)

Pedagogical lambda-cube: the λ2 case. - Vincent Demange (J. Log. Comput., 2015)