Home

Publications

Évelyne Contejean

contejean

2011

[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 ]

2010

[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 ]

2008

[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 ]

2007

[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 ]

2005

[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 ]

2004

[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 ]

2003

[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 ]

2001

[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 ]

2000

[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 ]

1998

[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 ]

1997

[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 ]

1996

[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 ]

1995

[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 ]

1994

[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 ]

1993

[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 ]

1992

[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 ]

1991

[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 ]

1990

[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 ]

1989

[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 ]

1988

[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.