Selected Bibliography of H. Comon-Lundh (1989--2004)

Last update: November 2004.

Unpublished articles

H. Comon and V. Cortier. Tree automata with one memory, set constraints and cryptographic protocols Draft paper (98 pages)
H. Comon and Max Dauchet and R. Gilleron and D. Lugiez and S. Tison and M. Tommasi. Tree Automata Techniques and Applications . The current version of the book.
Hubert Comon and Yan Jurski . Counter automata, fixpoints and additive theories. Draft paper

2004

Hubert Comon-Lundh. Intruder Theories . Fossacs 2004, invited talk. The slides of the presentation.

2003

Hubert Comon-Lundh and Ralf Treinen. Easy Intruder Deductions . In Verification:Theory and Practice , essays dedicated to Zohar Manna. LNCS series 2772, © Springer-Verlag, 2003.
Hubert Comon, Paliath Narendran, Robert Nieuwenhuis and Michael Rusinowitch , Deciding the confluence of ordered term rewrite systems ACM Transactions on Computational Logic 4(1), 2003. © ACM press
Hubert Comon-Lundh, Véronique Cortier , Security properties: two agents are sufficient , Proc. European Symposium on Programming, LNCS series 2618, © Springer-Verlag, 2003.
Hubert Comon-Lundh, Véronique Cortier , New decidability results for fragments of first-order logic and application to cryptographic protocols , Proc. Rewriting Techniques and applications, LNCS series , © Springer-Verlag, 2003.
Hubert Comon-Lundh, Vitaly Shmatikov , Intruder deductions, constraint solving and insecurity decision in presence of exclusive or , Proc. Symp. on Logic in Computer Science (LICS'03), © IEEE Computer Society Press, 2003.

2002

H. Comon and V. Shmatikov. Is it possible to decide whether a cryptographic protocol is secure or not ? Journal of Telecommunications and Information Technology 4, 2002.

2001

Hubert Comon . Inductionless Induction. Handbook of Automated Reasoning, chapter 14, © Elsevier, 2001 Draft handbook chapter.
H. Comon, V. Cortier, and J. Mitchell. Tree automata with one memory, set constraints and ping-pong protocols. In Proc. 28th Int. Coll. Automata, Languages, and Programming (ICALP'2001), Crete, Greece, July 2001, volume 2076 of LNCS series , pages 682-693. © Springer-Verlag, 2001.
H. Comon, G. Godoy, and R. Nieuwenhuis. The confluence of ground term rewrite systems is decidable in polynomial time. In Proc. 42nd Symp. Foundations of Computer Science (FOCS'2001), Las Vegas, NV, USA, Oct. 2001. © IEEE Comp. Soc. Press, 2001.

2000

Hubert Comon and Véronique Cortier, Flatness is not a weakness ,
Proc. Computer Science Logic, 2000 , LNCS series . abstract paper © Springer-Verlag.
Hubert Comon and Robert Nieuwenhuis, Induction=I-axiomatixation+first-order consistency .
Information and Computation full paper © Academic Press.
Hubert Comon, Sequentiality, Monadic Second Order Logic and Tree Automata , Information and Computation
BibTeX entry , full paper © Academic Press.

1999

H. Comon and Yan Jurski Timed Automata and the Theory of Real Numbers . Proc. CONCUR 99. LNCS series "© Springer-Verlag".
BibTeX entry , The full version of the paper (LSV research report).
Hubert Comon, Mehmet Dincbas, Jean-Pierre Jouannaud, and Claude Kirchner. A methodological view of constraint solving. Constraints 4(4) .
BibTeX entry, abstract, full paper

1998

Hubert Comon and Paliath Narendran and Robert Nieuwenhuis and Michael Rusinowitch. Decision problems in ordered rewriting Proc. IEEE Symp. on Logic in Computer Science, Indianapolis , 1998
Abstract paper , BibTeX entry , long version
Hubert Comon and Yan Jurski. Multiple counters automata, safety analysis and Presburger arithmetic, Proc. Computer Aided Verification, Vancouver , 1998
Abstract paper , BibTeX entry , long version (research report)
H. Comon. Completion of rewrite systems with membership constraints. part i: deduction rules. Journal of Symbolic Computation.
BibTeX entry, full paper
H. Comon. Completion of rewrite systems with membership constraints. part ii: Constraint solving. Journal of Symbolic Computation.
BibTeX entry, full paper

1997

Hubert Comon and Yan Jurski. Higher-order matching and tree automata . In Proc. CSL'97, LNCS. BibTeX entry, full paper
Hubert Comon and Florent Jacquemard Ground reducibility is EXPTIME-complete Proc. IEEE Symp. Logic in Computer Science, Varsaw , 1997
BibTeX entry , Abstract paper , long version (research report).
Hubert Comon and Ralf Treinen. The first-order theory of lexicographic path orderings is undecidable. Theoretical Computer Science, 1997.
BibTeX entry, abstract, full paper

1996

Alexandre Boudet and Hubert Comon. Diophantine Equations, Presburger Arithmetic and Finite Automata. Proc. CAAP 96 . BibTeX entry,

1995

Hubert Comon. On unification of terms with integer exponents. Math. Systems Theory, 28:67-88, 1995.
BibTeX entry, full paper
Hubert Comon. Sequentiality, second-order monadic logic and tree automata. In Tenth Annual IEEE Symposium on Logic in Computer Science, San Diego, CA, June 1995. IEEE Comp. Soc. Press.
BibTeX entry, abstract, full paper
Hubert Comon, Robert Nieuwenhuis, and Albert Rubio. Orderings, AC-theories and symbolic constraint solving. In Tenth Annual IEEE Symposium on Logic in Computer Science, pages 375-385, San Diego, CA, June 1995. IEEE Comp. Soc. Press.
BibTeX entry, abstract, full paper

1994

A.-C. Caron, H. Comon, J.-L. Coquidé, M. Dauchet, and F. Jacquemard. Pumping, cleaning and symbolic constraints solving. In Proc. Int. Conference on Algorithms, Languages and Programming, Jerusalem, July 1994.
BibTeX entry
Hubert Comon and Catherine Delor. Equational formulae with membership constraints. Information and Computation, 112(2):167-216, August 1994.
BibTeX entry, abstract, full paper
Hubert Comon, Marianne Haberstrau, and Jean-Pierre Jouannaud. Syntacticness, cycle-syntacticness and shallow theories. Information and Computation, 111(1):154-191, May 1994.
BibTeX entry, full paper
Hubert Comon and Florent Jacquemard. Ground reducibility and automata with disequality constraints. In P. Enjalbert, editor, Proc. 11th Symp. on Theoretical Aspects of Computer Science, Caen, 1994. Springer-Verlag.
BibTeX entry
Hubert Comon and Ralf Treinen. Ordering constraints on trees. In S. Tison, editor, Proc. CAAP 94, LNCS, Edinburgh, April 1994. Springer Verlag. (Invited Lecture).
BibTeX entry, full paper
H. Comon. Inductionless induction. Lecture notes. Int. summer school on automated deduction, Chambéry, July 1994.
BibTeX entry, full paper
S. Cerrito, H. Comon and C. Crépeau. Calculabilité et complexité . Notes du cours de C3, maîtrise d'informatique de Paris 11.
BibTeX entry , full paper

1993

Hubert Comon. Complete axiomatizations of some quotient term algebras. Theoretical Computer Science, 118(2), September 1993.
BibTeX entry, full paper
Hubert Comon. Constraints in term algebras (short survey). In T. Rus M. Nivat, C. Rattray and G. Scollo, editors, Proc. Conf. on Algebraic Methodology and Software Technology, Univ. of Twente, 1993. Springer Verlag, series Workshop in Computing. Invited talk.
BibTeX entry, full paper
Alexandre Boudet and Hubert Comon About the Theory of Tree Embedding . in Proc. Int. Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Orsay, 1993. LNCS 668.
BibTeX entry , full paper .

1992

Hubert Comon. Completion of rewrite systems with membership constraints. In W. Kuich, editor, Proc. 19th Int. Coll. on Automata, Languages and Programming, LNCS 623, Vienna, 1992. Springer-Verlag.
BibTeX entry
Hubert Comon. Constraints in term algebras. application to rewrite systems. Atti Degli Incontri Di Logica Matematica, 8:5-17, 1992.
BibTeX entry
Hubert Comon. Resolution de contraintes dans des algebres de termes: rapport d'habilitation. Technical Report 751, LRI, Univ. Paris-Sud, 1992.
BibTeX entry, full paper
Hubert Comon and Maribel Fernández. Negation elimination in equational formulae. In Proc. 17th Mathematical Foundations of Computer Science, Praha, LNCS, 1992.
BibTeX entry
Hubert Comon, Marianne Haberstrau, and Jean-Pierre Jouannaud. Decidable properties of shallow equational theories. In Proc. 7th IEEE Symp. Logic in Computer Science, Santa Cruz, 1992.
BibTeX entry

1991

Hubert Comon. Complete axiomatizations of some quotient term algebras. In Proc. 18th Int. Coll. on Automata, Languages and Programming, Madrid, LNCS 510, July 1991.
BibTeX entry
Hubert Comon. Disunification: a survey. In Jean-Louis Lassez and Gordon Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1991.
BibTeX entry, full paper
Hubert Comon. Ground normal forms and inductive proofs. part I: complement problems. Research Report 698, Laboratoire de Recherche en Informatique, 1991.
BibTeX entry
Hubert Comon, Denis Lugiez, and Philippe Schnoebelen. A rewrite-based type discipline for a subset of computer algebra. Journal of Symbolic Computation, 11, 1991.
BibTeX entry

1990

Hubert Comon. Equational formulas in order-sorted algebras. In Proc. 17th Int. Coll. on Automata, Languages and Programming, Warwick, LNCS 443, Warwick, July 1990. Springer-Verlag.
BibTeX entry
Hubert Comon. Solving inequations in term algebras. In Proc. 5th IEEE Symp. Logic in Computer Science, Philadelphia, June 1990.
BibTeX entry
Hubert Comon. Solving symbolic ordering constraints. International Journal of Foundations of Computer Science, 1(4):387-411, 1990.
BibTeX entry, full paper

1989

Hubert Comon. Inductive proofs by specifications transformation. In Proc. 3rd Rewriting Techniques and Applications, Chapel Hill, LNCS 355, pages 76-91. Springer-Verlag, April 1989.
BibTeX entry
Hubert Comon and Pierre Lescanne. Equational problems and disunification. Journal of Symbolic Computation, 7:371-425, 1989.
BibTeX entry