Handling Polymorphism in Automated Deduction. - Jean-François Couchot; Stéphane Lescuyer (CADE, 2007)

CC(X): Semantic Combination of Congruence Closure with Solvable Theories. - Sylvain Conchon; Evelyne Contejean; Johannes Kanig; Stéphane Lescuyer (SMT@CAV, 2007)

Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme. - Stéphane Lescuyer; Sylvain Conchon (FroCoS, 2009)

Faire bonne figure avec MLPOST. - Romain Bardou; Jean-Christophe Filliâtre; Johannes Kanig; Stéphane Lescuyer (Stud. Inform. Univ., 2009)

First-Class Containers in Coq. - Stéphane Lescuyer (Stud. Inform. Univ., 2011)

Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq. (Formalisation et developpement d'une tactique reflexive pour la demonstration automatique en coq). - Stéphane Lescuyer (2011)

ProvenCore: Towards a Verified Isolation Micro-Kernel. - Stéphane Lescuyer (MILS@HiPEAC, 2015)

Dependency Analysis of Functional Specifications with Algebraic Data Structures. - Oana Fabiana Andreescu; Thomas P. Jensen; Stéphane Lescuyer (ICFEM, 2015)

Correlating Structured Inputs and Outputs in Functional Specifications. - Oana Fabiana Andreescu; Thomas P. Jensen; Stéphane Lescuyer (SEFM, 2016)

Inferring frame conditions with static correlation analysis. - Oana Fabiana Andreescu; Thomas P. Jensen; Stéphane Lescuyer; Benoît Montagu (Proc. ACM Program. Lang., 2019)