Evelyne Contejean

Mohammed Houssem Hachmaoui

Proc. ACM Program. Lang., 2022

2021

A Coq formalization of data provenance.

[BibT_eX]

[DOI]

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2019

A Coq mechanised formal semantics for realistic SQL queries: formally reconciling SQL and bag relational algebra.

[BibT_eX]

[DOI]

Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2019

2018

A Coq Formalisation of SQL's Execution Engines.

[BibT_eX]

[DOI]

Proceedings of the Interactive Theorem Proving - 9th International Conference, 2018

2017

Certifying Standard and Stratified Datalog Inference Engines in SSReflect.

[BibT_eX]

[DOI]

Stefania Dumbrava

Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

2014

A Coq Formalization of the Relational Data Model.

[BibT_eX]

[DOI]

Stefania Dumbrava

Proceedings of the Programming Languages and Systems, 2014

Facettes de la preuve : Jeux de reflets entre démonstration automatique et preuve assistée.

[BibT_eX]

[DOI]

, 2014

2012

Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation

[BibT_eX]

[DOI]

Sylvain Conchon

Mohamed Iguernelala

Log. Methods Comput. Sci., 2012

A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

Canonized Rewriting and Ground AC Completion Modulo Shostak Theories.

[BibT_eX]

[DOI]

Sylvain Conchon

Mohamed Iguernelala

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2011

Automated Certified Proofs with CiME3.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

2010

A3PAT, an approach for certified automated termination proofs.

[BibT_eX]

[DOI]

Proceedings of the 2010 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2010

Ground Associative and Commutative Completion Modulo Shostak Theories.

[BibT_eX]

[DOI]

Sylvain Conchon

Mohamed Iguernelala

Proceedings of the Short papers for 17th International Conference on Logic for Programming, 2010

2007

CC(X): Semantic Combination of Congruence Closure with Solvable Theories.

[BibT_eX]

[DOI]

Proceedings of the 5th International Workshop on Satisfiability Modulo Theories, 2007

Certification of Automated Termination Proofs.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 6th International Symposium, 2007

Modeling Permutations in Coqfor Coccinelle.

[BibT_eX]

[DOI]

Proceedings of the Rewriting, 2007

2005

Mechanically Proving Termination Using Polynomial Interpretations.

[BibT_eX]

[DOI]

J. Autom. Reason., 2005

Reflecting Proofs in First-Order Logic with Equality.

[BibT_eX]

[DOI]

Pierre Corbineau

Proceedings of the Automated Deduction, 2005

2004

A Certified AC Matching Algorithm.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 15th International Conference, 2004

2001

Combining Pattern E-Unification Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 12th International Conference, 2001

2000

Rewriting Techniques in Theoretical Physics.

[BibT_eX]

[DOI]

Antoine Coste

Benjamin Monate

Proceedings of the Rewriting Techniques and Applications, 11th International Conference, 2000

1998

About the Confluence of Equational Pattern Rewrite Systems.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1998

1997

Avoiding Slack Variables in the Solving of Linear Diophantine Equations and Inequations.

[BibT_eX]

[DOI]

Farid Ajili

Theor. Comput. Sci., 1997

Rewrite Systems for Natural, Integral, and Rational Arithmetic.

[BibT_eX]

[DOI]

Claude Marché

Landy Rabehasaina

Proceedings of the Rewriting Techniques and Applications, 8th International Conference, 1997

AC-Unification of Higher-Order Patterns.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming - CP97, Third International Conference, Linz, Austria, October 29, 1997

1996

CiME: Completion Modulo E.

[BibT_eX]

[DOI]

Claude Marché

Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

AC-Complete Unification and its Application to Theorem Proving.

[BibT_eX]

[DOI]

Claude Marché

Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

1995

Complete Solving of Linear Diophantine Equations and Inequations without Adding Slack Variables.

[BibT_eX]

Farid Ajili

Proceedings of the 9th International Workshop on Unification, 1995

Complete Solving of Linear Diophantine Equations and Inequations without Adding Variables.

[BibT_eX]

[DOI]

Farid Ajili

Proceedings of the Principles and Practice of Constraint Programming, 1995

1994

An Efficient Incremental Algorithm for Solving Systems of Linear Diophantine Equations

[BibT_eX]

[DOI]

Hervé Devie

Inf. Comput., August, 1994

"Syntactic" AC-Unification.

[BibT_eX]

[DOI]

Proceedings of the Constraints in Computational Logics, First International Conference, 1994

1993

Solving *-Problems Modulo Distributivity by a Reduction to AC1-Unification.

[BibT_eX]

[DOI]

J. Symb. Comput., 1993

Solving Linear Diophantine Constraints Incrementally.

[BibT_eX]

Proceedings of the Logic Programming, 1993

A Partial Solution for D-Unification Based on a Reduction to AC1-Unification.

[BibT_eX]

[DOI]

Proceedings of the Automata, Languages and Programming, 20nd International Colloquium, 1993

1992

On n-Syntactic Equational Theories.

[BibT_eX]

[DOI]

Proceedings of the Algebraic and Logic Programming, 1992

1990

A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations

[BibT_eX]

[DOI]