| 2021 | CPP | A Coq formalization of data provenance. | Vronique Benzaken, Sarah Cohen-Boulakia, Evelyne Contejean, Chantal Keller, Rbecca Zucchini |
| 2019 | CPP | A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. | Vronique Benzaken, Evelyne Contejean |
| 2018 | ITP | A Coq Formalisation of SQL's Execution Engines. | Vronique Benzaken, Evelyne Contejean, Chantal Keller, Eunice Martins |
| 2017 | ITP | Certifying Standard and Stratified Datalog Inference Engines in SSReflect. | Vronique Benzaken, Evelyne Contejean, Stefania Dumbrava |
| 2014 | ESOP | A Coq Formalization of the Relational Data Model. | Vronique Benzaken, Evelyne Contejean, Stefania Dumbrava |
| 2012 | CADE | A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. | Franois Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, Guillaume Melquiond |
| 2011 | TACAS | Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. | Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala |
| 2010 | LPAR | Ground Associative and Commutative Completion Modulo Shostak Theories. | Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala |
| 2010 | PEPM | A3PAT, an approach for certified automated termination proofs. | Evelyne Contejean, Andrey Paskevich, Xavier Urbain, Pierre Courtieu, Olivier Pons, Julien Forest |
| 2005 | CADE | Reflecting Proofs in First-Order Logic with Equality. | Evelyne Contejean, Pierre Corbineau |
| 1998 | CADE | About the Confluence of Equational Pattern Rewrite Systems. | Alexandre Boudet, Evelyne Contejean |
| 1997 | CP | AC-Unification of Higher-Order Patterns. | Alexandre Boudet, Evelyne Contejean |
| 1995 | CP | Complete Solving of Linear Diophantine Equations and Inequations without Adding Variables. | Farid Ajili, Evelyne Contejean |
| 1993 | ICALP | A Partial Solution for D-Unification Based on a Reduction to AC1-Unification. | Evelyne Contejean |
| 1993 | ICLP | Solving Linear Diophantine Constraints Incrementally. | Evelyne Contejean |
| 1990 | LICS | A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations | Alexandre Boudet, Evelyne Contejean, Herv Devie |