Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. - Denis Cousineau 002; Gilles Dowek (TLCA, 2007)

Modèles et normalisation des preuves. (Models and proof normalization). - Denis Cousineau 002 (2009)

TLA + Proofs. - Denis Cousineau 002; Damien Doligez; Leslie Lamport; Stephan Merz; Daniel Ricketts 001; Hernán Vanzetto (FM, 2012)

A Semantic Proof that Reducibility Candidates entail Cut Elimination. - Denis Cousineau 002; Olivier Hermant (RTA, 2012)

On completeness of reducibility candidates as a semantics of strong normalization - Denis Cousineau 002 (Log. Methods Comput. Sci., 2012)

Fast, Automatic, and Nearly Complete Structural Unit-Test Generation Combining Genetic Algorithms and Formal Methods. - Eric Lavillonnière; David Mentré; Denis Cousineau 002 (TAP@FM, 2019)

Automated Deductive Verification for Ladder Programming. - Denis Cousineau 002; David Mentré; Hiroaki Inoue (F-IDE@FM, 2019)

Automated Verification of Temporal Properties of Ladder Programs. - Cláudio Belo Lourenço; Denis Cousineau 002; Florian Faissole; Claude Marché; David Mentré; Hiroaki Inoue (FMICS, 2021)

Modular pre-processing for automated reasoning in dependent type theory. - Valentin Blot; Denis Cousineau 002; Enzo Crance; Louise Dubois de Prisque; Chantal Keller; Assia Mahboubi; Pierre Vial (CoRR, 2022)

Automated formal analysis of temporal properties of Ladder programs. - Cláudio Belo Lourenço; Denis Cousineau 002; Florian Faissole; Claude Marché; David Mentré; Hiroaki Inoue (Int. J. Softw. Tools Technol. Transf., 2022)

Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. - Valentin Blot; Denis Cousineau 002; Enzo Crance; Louise Dubois de Prisque; Chantal Keller; Assia Mahboubi; Pierre Vial (CPP, 2023)