PublicationsÉvelyne Contejean |
[1] |
Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala.
Canonized Rewriting and Ground AC Completion Modulo Shostak
Theories.
In Parosh A. Abdulla and K. Rustan M. Leino, editors, Tools and
Algorithms for the Construction and Analysis of Systems, volume 6605 of
Lecture Notes in Computer Science, pages 45-59, Saarbrücken, Germany,
April 2011. Springer. [ bib | DOI | Abstract ] |
[2] |
Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier
Urbain.
Automated Certified Proofs with CiME3.
In Manfred Schmidt-Schauß, editor, 22nd International
Conference on Rewriting Techniques and Applications (RTA 11), volume 10 of
Leibniz International Proceedings in Informatics (LIPIcs), pages
21-30, Novi Sad, Serbia, 2011. Schloss Dagstuhl-Leibniz-Zentrum fuer
Informatik. [ bib | DOI | Abstract ] |
[3] |
Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier
Urbain.
Automated Certified Proofs with CiME3.
Technical Report 2044, Cédric laboratory, CNAM Paris, France, 2011. [ bib | Url | Abstract ] |
[4] |
Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala.
Canonized Rewriting and Ground AC Completion Modulo Shostak
Theories.
Research Report 1538, LRI, Université Paris Sud, December 2010. [ bib | url | Abstract ] |
[5] |
Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala.
Ground Associative and Commutative Completion Modulo Shostak
Theories.
In Andrei Voronkov, editor, LPAR, 17th International Conference
on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair
Proceedings, Yogyakarta, Indonesia, October 2010.
(short paper). [ bib ] |
[6] |
Évelyne Contejean, Pierre Courtieu, Julien Forest, Andrei Paskevich, Olivier
Pons, and Xavier Urbain.
A3PAT, an Approach for Certified Automated Termination Proofs.
In John P. Gallagher and Janis Voigtländer, editors, Partial
Evaluation and Program Manipulation, pages 63-72, Madrid, Spain, January
2010. ACM Press. [ bib | DOI | Abstract ] |
[7] |
Évelyne Contejean and Xavier Urbain.
The A3PAT approach.
In Workshop on Certified Termination WScT08, Leipzig, Germany,
May 2008. [ bib ] |
[8] |
Évelyne Contejean.
Coccinelle, a Coq library for rewriting.
In Types, Torino, Italy, March 2008. [ bib ] |
[9] |
François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane
Lescuyer.
Implementing Polymorphism in SMT solvers.
In Clark Barrett and Leonardo de Moura, editors, SMT 2008: 6th
International Workshop on Satisfiability Modulo, volume 367 of ACM
International Conference Proceedings Series, pages 1-5, 2008. [ bib | DOI | Abstract ] |
[10] |
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer.
CC(X): Semantical combination of congruence closure with solvable
theories.
In Post-proceedings of the 5th International Workshop on
Satisfiability Modulo Theories (SMT 2007), volume 198(2) of
Electronic Notes in Computer Science, pages 51-69. Elsevier Science
Publishers, 2008. [ bib | DOI | Abstract ] |
[11] |
François Bobot, Sylvain Conchon, Évelyne Contejean, Mohamed Iguernelala,
Stéphane Lescuyer, and Alain Mebsout.
The Alt-Ergo automated theorem prover, 2008.
APP deposit under the number IDDN FR 001 110026 000 S P 2010 000
1000. [ bib | Url ] |
[12] |
Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier
Urbain.
Certification of automated termination proofs.
In Boris Konev and Frank Wolter, editors, 6th International
Symposium on Frontiers of Combining Systems (FroCos 07), volume 4720 of
Lecture Notes in Artificial Intelligence, pages 148-162, Liverpool,UK,
September 2007. Springer. [ bib | DOI | Abstract ] |
[13] |
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane
Lescuyer.
Lightweight Integration of the Ergo Theorem Prover inside a Proof
Assistant.
In John Rushby and N. Shankar, editors, Proceedings of the
second workshop on Automated formal methods, pages 55-59. ACM Press, 2007. [ bib | DOI | url | Abstract ] |
[14] |
Sylvain Conchon, Évelyne Contejean, and Johannes Kanig.
CC(X): Efficiently combining equality and solvable theories without
canonizers.
In Sava Krstic and Albert Oliveras, editors, SMT 2007: 5th
International Workshop on Satisfiability Modulo, 2007. [ bib ] |
[15] |
Évelyne Contejean.
Modelling permutations in Coq for Coccinelle.
In Hubert Comon-Lundth, Claude Kirchner, and Hélène Kirchner,
editors, Rewriting, Computation and Proof, volume 4600 of Lecture
Notes in Computer Science, pages 259-269. Springer, 2007.
Jouannaud Festschrift. [ bib | DOI | Abstract ] |
[16] |
Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons, and Xavier
Urbain.
CiME3, 2007.
http://cime.lri.fr. [ bib | Url ] |
[17] |
Évelyne Contejean and Pierre Corbineau.
Reflecting proofs in first-order logic with equality.
In Robert Nieuwenhuis, editor, 20th International Conference on
Automated Deduction (CADE-20), volume 3632 of Lecture Notes in
Artificial Intelligence, pages 7-22, Tallinn, Estonia, July 2005. Springer. [ bib | DOI | Abstract ] |
[18] |
Évelyne Contejean, Claude Marché, Ana Paula Tomás, and Xavier Urbain.
Mechanically proving termination using polynomial interpretations.
Journal of Automated Reasoning, 34(4):325-363, 2005. [ bib | DOI | Abstract ] |
[19] |
Évelyne Contejean.
Coccinelle, 2005. [ bib | Url ] |
[20] |
Évelyne Contejean, Claude Marché, Ana-Paula Tomás, and Xavier Urbain.
Mechanically proving termination using polynomial interpretations.
Research Report 1382, LRI, 2004. [ bib | Url ] |
[21] |
Évelyne Contejean.
A certified AC matching algorithm.
In Vincent van Oostrom, editor, 15th International Conference on
Rewriting Techniques and Applications, volume 3091 of Lecture Notes in
Computer Science, pages 70-84, Aachen, Germany, June 2004. Springer. [ bib | DOI | Abstract ] |
[22] |
Évelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain.
Proving Termination of Rewriting with CiME.
In Albert Rubio, editor, Extended Abstracts of the 6th
International Workshop on Termination, WST'03, pages 71-73, June 2003.
Technical Report DSIC II/15/03, Universidad Politécnica de
Valencia, Spain. [ bib | Url ] |
[23] |
Évelyne Contejean and Ana Paula Tomas.
On Symmetries in Systems Coming from AC-Unification of Higher-Order
Patterns.
In Pierre Flener and Justin Pearson, editors, SymCon'01,
Symmetry in Constraints, Paphos, Cyprus, December 2001. [ bib ] |
[24] |
Alexandre Boudet and Evelyne Contejean.
Combining Pattern E-unification Algorithms.
In Aart Middeldorp, editor, 12th International Conference on
Rewriting Techniques and Applications, volume 2051 of Lecture Notes in
Computer Science, pages 63-76, Utrecht, The Netherlands, May 2001.
Springer. [ bib | DOI | Abstract ] |
[25] |
Evelyne Contejean, Claude Marché, Benjamin Monate, and Xavier Urbain.
CiME version 2, 2000.
Available at http://cime.lri.fr/. [ bib | Url ] |
[26] |
Évelyne Contejean, Antoine Coste, and Benjamin Monate.
Rewriting techniques in theoretical physics.
In Leo Bachmair, editor, 11th International Conference on
Rewriting Techniques and Applications, volume 1833 of Lecture Notes in
Computer Science, pages 80-94, Norwich, UK, July 2000. Springer. [ bib | DOI | Abstract ] |
[27] |
Alexandre Boudet and Evelyne Contejean.
About the Confluence of Equational Pattern Rewrite Systems.
In C. and H. Kirchner, editors, 15th International Conference on
Automated Deduction, volume 1421 of Lecture Notes in Computer Science,
pages 88-102, Lindau, Germany, July 1998. Springer. [ bib | DOI | Abstract ] |
[28] |
Nicolas Beldiceanu, Eric Bourreau, and Evelyne Contejean.
Solving a hard vehicle routing & loading problem.
In Proceedings of the Spring Meeting of the Institute for
Operations Research and the Management Sciences, Montreal, April 1998. [ bib | Abstract ] |
[29] |
Alexandre Boudet and Evelyne Contejean.
AC-unification of higher-order patterns.
In Gert Smolka, editor, Principles and Practice of Constraint
Programming, volume 1330 of Lecture Notes in Computer Science, pages
267-281, Linz, Austria, October 1997. Springer. [ bib | DOI | Abstract ] |
[30] |
Evelyne Contejean, Claude Marché, and Landy Rabehasaina.
Rewrite systems for natural, integral, and rational arithmetic.
In Hubert Comon, editor, 8th International Conference on
Rewriting Techniques and Applications, volume 1232 of Lecture Notes in
Computer Science, pages 98-112, Barcelona, Spain, June 1997. Springer. [ bib | DOI | Abstract ] |
[31] |
Farid Ajili and Evelyne Contejean.
Avoiding slack variables in the solving of linear diophantine
equations and inequations.
Theoretical Computer Science, 173(1):183-208, February 1997. [ bib | DOI | Abstract ] |
[32] |
Alexandre Boudet, Evelyne Contejean, and Claude Marché.
AC-complete unification and its application to theorem proving.
In Harald Ganzinger, editor, 7th International Conference on
Rewriting Techniques and Applications, volume 1103 of Lecture Notes in
Computer Science, pages 18-32, New Brunswick, NJ, USA, July 1996. Springer. [ bib | DOI | Abstract ] |
[33] |
Evelyne Contejean and Claude Marché.
CiME: Completion Modulo E.
In Harald Ganzinger, editor, 7th International Conference on
Rewriting Techniques and Applications, volume 1103 of Lecture Notes in
Computer Science, pages 416-419, New Brunswick, NJ, USA, July 1996.
Springer.
System Description available at http://cime.lri.fr/. [ bib | DOI | Url | Abstract ] |
[34] |
Farid Ajili and Evelyne Contejean.
Complete solving of linear diophantine equations and inequations
without adding variables.
In Ugo Montanari and Francesca Rossi, editors, Proc. First
International Conference on Principles and Practice of Constraint
Programming, volume 976 of Lecture Notes in Computer Science, pages
1-17, Cassis, France, September 1995. Springer. [ bib | DOI | Abstract ] |
[35] |
Alexandre Boudet and Evelyne Contejean.
“Syntactic” AC-unification.
In Jean-Pierre Jouannaud, editor, First International Conference
on Constraints in Computational Logics, volume 845 of Lecture Notes in
Computer Science, pages 136-151, München, Germany, September 1994.
Springer. [ bib | DOI | Abstract ] |
[36] |
Evelyne Contejean and Hervé Devie.
An efficient algorithm for solving systems of diophantine equations.
Information and Computation, 113(1):143-172, August 1994. [ bib | DOI | Abstract ] |
[37] |
Nicolas Beldiceanu and Evelyne Contejean.
Introducing global constraints in CHIP.
Journal of Mathematical and Computer Modelling,
20(12):97-123, 1994. [ bib | DOI | Abstract ] |
[38] |
Evelyne Contejean.
Solving linear diophantine constraints incrementally.
In David S. Warren, editor, Proceedings of the 10th
International Conference on Logic Programming, Logic Programming, pages
532-549, Budapest, Hungary, June 1993. MIT Press. [ bib | Url | Abstract ] |
[39] |
Nicolas Beldiceanu, Evelyne Contejean, and Helmut Simonis.
Integrating an algorithm for solving linear constraints in finite
domains in the language CHIP.
In Proc. 4th Workshop on Constraint Logic Programming, March
1993. [ bib | Abstract ] |
[40] |
Evelyne Contejean.
A partial solution for D-unification based on a reduction to
AC1-unification.
In Andrzej Lingas, Rolf Karlsson, and Svante Carlsson, editors,
20th International Colloquium on Automata, Languages and Programming, volume
700 of Lecture Notes in Computer Science, pages 621-632, Lund, Sweden,
July 1993. Springer. [ bib | DOI | Abstract ] |
[41] |
Evelyne Contejean.
Solving *-problems modulo distributivity by a reduction to
AC1-unification.
Journal of Symbolic Computation, 16(5):493-52, 1993. [ bib | DOI | Abstract ] |
[42] |
Alexandre Boudet and Evelyne Contejean.
On n-syntactic equational theories.
In Hélène Kirchner and Giorgio Levi, editors, 3th
International Conference on Algebraic and Logic Programming, volume 632 of
Lecture Notes in Computer Science, pages 446-457, Volterra, Italy,
September 1992. Springer. [ bib | DOI | Abstract ] |
[43] |
Evelyne Contejean.
Éléments pour la Décidabilité de l'Unification
modulo la Distributivité.
Thèse de doctorat, Université Paris-Sud, Orsay, France, April
1992. [ bib ] |
[44] |
Evelyne Contejean and Hervé Devie.
Résolution de systèmes linéaires d'équations
diophantiennes.
Comptes-Rendus de l'Académie des Sciences de Paris,
313:115-120, 1991.
Série I. [ bib | Abstract ] |
[45] |
Alexandre Boudet, Evelyne Contejean, and Hervé Devie.
A new AC-unification algorithm with a new algorithm for solving
diophantine equations.
In Proceedings of the Fifth Annual IEEE Symposium on Logic in
Computer Science, pages 289-299, Philadelphia, Pennsylvania, USA, June
1990. IEEE Comp. Soc. Press. [ bib | DOI | Abstract ] |
[46] |
Evelyne Contejean and Hervé Devie.
Solving systems of linear diophantine equations.
In Proc. 3rd Workshop on Unification, Lambrecht, Germany.
University of Kaiserslautern, June 1989. [ bib ] |
[47] |
Evelyne Contejean.
Unification associative-commutative.
Mémoire de DEA , Université de Paris Sud, Orsay, 1988. [ bib ] |
This document was translated from LATEX by HEVEA.