A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations - Alexandre Boudet; Evelyne Contejean; Hervé Devie (LICS, 1990)

On n-Syntactic Equational Theories. - Alexandre Boudet; Evelyne Contejean (ALP, 1992)

A Partial Solution for D-Unification Based on a Reduction to AC1-Unification. - Evelyne Contejean (ICALP, 1993)

Solving Linear Diophantine Constraints Incrementally. - Evelyne Contejean (ICLP, 1993)

Solving *-Problems Modulo Distributivity by a Reduction to AC1-Unification. - Evelyne Contejean (J. Symb. Comput., 1993)

"Syntactic" AC-Unification. - Alexandre Boudet; Evelyne Contejean (CCL, 1994)

An Efficient Incremental Algorithm for Solving Systems of Linear Diophantine Equations - Evelyne Contejean; Hervé Devie (Inf. Comput., 1994)

Complete Solving of Linear Diophantine Equations and Inequations without Adding Variables. - Farid Ajili; Evelyne Contejean (CP, 1995)

Complete Solving of Linear Diophantine Equations and Inequations without Adding Slack Variables. - Farid Ajili; Evelyne Contejean (UNIF, 1995)

AC-Complete Unification and its Application to Theorem Proving. - Alexandre Boudet; Evelyne Contejean; Claude Marché (RTA, 1996)

CiME: Completion Modulo E. - Evelyne Contejean; Claude Marché (RTA, 1996)

AC-Unification of Higher-Order Patterns. - Alexandre Boudet; Evelyne Contejean (CP, 1997)

Rewrite Systems for Natural, Integral, and Rational Arithmetic. - Evelyne Contejean; Claude Marché; Landy Rabehasaina (RTA, 1997)

Avoiding Slack Variables in the Solving of Linear Diophantine Equations and Inequations. - Farid Ajili; Evelyne Contejean (Theor. Comput. Sci., 1997)

About the Confluence of Equational Pattern Rewrite Systems. - Alexandre Boudet; Evelyne Contejean (CADE, 1998)

Rewriting Techniques in Theoretical Physics. - Evelyne Contejean; Antoine Coste; Benjamin Monate (RTA, 2000)

Combining Pattern E-Unification Algorithms. - Alexandre Boudet; Evelyne Contejean (RTA, 2001)

A Certified AC Matching Algorithm. - Evelyne Contejean (RTA, 2004)

Reflecting Proofs in First-Order Logic with Equality. - Evelyne Contejean; Pierre Corbineau (CADE, 2005)

Mechanically Proving Termination Using Polynomial Interpretations. - Evelyne Contejean; Claude Marché; Ana Paula Tomás; Xavier Urbain (J. Autom. Reason., 2005)

Modeling Permutations in Coqfor Coccinelle. - Evelyne Contejean (Rewriting, Computation and Proof, 2007)

Certification of Automated Termination Proofs. - Evelyne Contejean; Pierre Courtieu; Julien Forest; Olivier Pons; Xavier Urbain (FroCoS, 2007)

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

Ground Associative and Commutative Completion Modulo Shostak Theories. - Sylvain Conchon; Evelyne Contejean; Mohamed Iguernelala (LPAR short papers(Yogyakarta), 2010)

A3PAT, an approach for certified automated termination proofs. - Evelyne Contejean; Andrey Paskevich; Xavier Urbain; Pierre Courtieu; Olivier Pons; Julien Forest (PEPM, 2010)

Automated Certified Proofs with CiME3. - Evelyne Contejean; Pierre Courtieu; Julien Forest; Olivier Pons; Xavier Urbain (RTA, 2011)

Canonized Rewriting and Ground AC Completion Modulo Shostak Theories. - Sylvain Conchon; Evelyne Contejean; Mohamed Iguernelala (TACAS, 2011)

A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. - François Bobot; Sylvain Conchon; Evelyne Contejean; Mohamed Iguernelala; Assia Mahboubi; Alain Mebsout; Guillaume Melquiond (IJCAR, 2012)

Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation - Sylvain Conchon; Evelyne Contejean; Mohamed Iguernelala (Log. Methods Comput. Sci., 2012)

Facettes de la preuve : Jeux de reflets entre démonstration automatique et preuve assistée. - Evelyne Contejean (2014)

A Coq Formalization of the Relational Data Model. - Véronique Benzaken; Evelyne Contejean; Stefania Dumbrava (ESOP, 2014)

Certifying Standard and Stratified Datalog Inference Engines in SSReflect. - Véronique Benzaken; Evelyne Contejean; Stefania Dumbrava (ITP, 2017)

A Coq Formalisation of SQL's Execution Engines. - Véronique Benzaken; Evelyne Contejean; Chantal Keller; Eunice Martins (ITP, 2018)

A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra. - Véronique Benzaken; Evelyne Contejean (CPP, 2019)

A Coq formalization of data provenance. - Véronique Benzaken; Sarah Cohen-Boulakia; Evelyne Contejean; Chantal Keller; Rébecca Zucchini (CPP, 2021)

Translating canonical SQL to imperative code in Coq. - Véronique Benzaken; Evelyne Contejean; Mohammed Houssem Hachmaoui; Chantal Keller; Louis Mandel; Avraham Shinnar; Jérôme Siméon (Proc. ACM Program. Lang., 2022)