Type Inference Using Unification in Computer Algebra. - Jacques Calmet; Hubert Comon; Denis Lugiez (AAECC, 1986)

Sufficient Completness, Term Rewriting Systems and "Anti-Unification". - Hubert Comon (CADE, 1986)

An Effective Method for Handling Initial Algebras. - Hubert Comon (ALP, 1988)

Unification et disunification : théorie et applications. (Unification and disunification in free algebras and in initial algebras : theory and applications). - Hubert Comon (1988)

Inductive Proofs by Specification Transformation. - Hubert Comon (RTA, 1989)

Equational Problems and Disunification. - Hubert Comon; Pierre Lescanne (J. Symb. Comput., 1989)

Equational Formulas in Order-Sorted Algebras. - Hubert Comon (ICALP, 1990)

Solving Inequations in Term Algebras (Extended Abstract) - Hubert Comon (LICS, 1990)

Solving Symbolic Ordering Constraints. - Hubert Comon (Int. J. Found. Comput. Sci., 1990)

Disunification: A Survey. - Hubert Comon (Computational Logic - Essays in Honor of Alan Robinson, 1991)

A Rewrite-Based Type Discipline for a Subset of Computer Algebra. - Hubert Comon; Denis Lugiez; Philippe Schnoebelen (J. Symb. Comput., 1991)

Completion of Rewrite Systems with Membership Constraints. - Hubert Comon (ICALP, 1992)

Decidable Problems in Shallow Equational Theories (Extended Abstract) - Hubert Comon; Marianne Haberstrau; Jean-Pierre Jouannaud (LICS, 1992)

Negation Elimination in Equational Formulae. - Hubert Comon; Maribel Fernández (MFCS, 1992)

Constraints in Term Algebras (Short Survey). - Hubert Comon (AMAST, 1993)

About the Theory of Tree Embedding. - Alexandre Boudet; Hubert Comon (TAPSOFT, 1993)

Complete Axiomatizations of Some Quotient Term Algebras. - Hubert Comon (Theor. Comput. Sci., 1993)

Ordering Constraints on Trees. - Hubert Comon; Ralf Treinen (CAAP, 1994)

Pumping, Cleaning and Symbolic Constraints Solving. - Anne-Cécile Caron; Hubert Comon; Jean-Luc Coquidé; Max Dauchet; Florent Jacquemard (ICALP, 1994)

Ground Reducibility and Automata with Disequality Constraints. - Hubert Comon; Florent Jacquemard (STACS, 1994)

Constraints in Term Algebras: An Overview of Constraint Solving Techniques - Hubert Comon (Constraint Programming, 1994)

Syntacticness, Cycle-Syntacticness, and Shallow Theories - Hubert Comon; Marianne Haberstrau; Jean-Pierre Jouannaud (Inf. Comput., 1994)

Equational Formulae with Membership Constraints - Hubert Comon; Catherine Delor (Inf. Comput., 1994)

Sequentiality, Second Order Monadic Logic and Tree Automata - Hubert Comon (LICS, 1995)

Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract) - Hubert Comon; Robert Nieuwenhuis; Albert Rubio (LICS, 1995)

Linear diophantine equations, Presburger arithmetic and finite automata. - Hubert Comon (UNIF, 1995)

On Unification of Terms with Integer Exponents. - Hubert Comon (Math. Syst. Theory, 1995)

Diophantine Equations, Presburger Arithmetic and Finite Automata. - Alexandre Boudet; Hubert Comon (CAAP, 1996)

Higher-Order Matching and Tree Automata. - Hubert Comon; Yan Jurski (CSL, 1997)

The First-Order Theory of Lexicographic Path Orderings is Undecidable. - Hubert Comon; Ralf Treinen (Theor. Comput. Sci., 1997)

Multiple Counters Automata, Safety Analysis and Presburger Arithmetic. - Hubert Comon; Yan Jurski (CAV, 1998)

Decision Problems in Ordered Rewriting. - Hubert Comon; Paliath Narendran; Robert Nieuwenhuis; Michaël Rusinowitch (LICS, 1998)

About Proofs by Consistency (Abstract). - Hubert Comon (RTA, 1998)

Completion of Rewrite Systems with Membership Constraints. Part I: Deduction Rules. - Hubert Comon (J. Symb. Comput., 1998)

Completion of Rewrite Systems with Membership Constraints. Part II: Constraint Solving. - Hubert Comon (J. Symb. Comput., 1998)

Constraint Solving on Terms. - Hubert Comon; Claude Kirchner (CCL, 1999)

Timed Automata and the Theory of Real Numbers. - Hubert Comon; Yan Jurski (CONCUR, 1999)

A Methodological View of Constraint Solving. - Hubert Comon; Mehmet Dincbas; Jean-Pierre Jouannaud; Claude Kirchner (Constraints An Int. J., 1999)

Flatness Is Not a Weakness. - Hubert Comon; Véronique Cortier (CSL, 2000)

Sequentiality, Monadic Second-Order Logic and Tree Automata. - Hubert Comon (Inf. Comput., 2000)

Induction=I-Axiomatization+First-Order Consistency. - Hubert Comon; Robert Nieuwenhuis (Inf. Comput., 2000)

Inductionless Induction. - Hubert Comon (Handbook of Automated Reasoning, 2001)

The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time. - Hubert Comon; Guillem Godoy; Robert Nieuwenhuis (FOCS, 2001)

Tree Automata with One Memory, Set Constraints, and Ping-Pong Protocols. - Hubert Comon; Véronique Cortier; John Mitchell (ICALP, 2001)

Easy Intruder Deductions. - Hubert Comon-Lundh; Ralf Treinen (Verification: Theory and Practice, 2003)

Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or. - Hubert Comon-Lundh; Vitaly Shmatikov (LICS, 2003)

New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols. - Hubert Comon-Lundh; Véronique Cortier (RTA, 2003)

Ground reducibility is EXPTIME-complete. - Hubert Comon; Florent Jacquemard (Inf. Comput., 2003)

Deciding the confluence of ordered term rewrite systems. - Hubert Comon; Paliath Narendran; Robert Nieuwenhuis; Michaël Rusinowitch (ACM Trans. Comput. Log., 2003)

Intruder Theories (Ongoing Work). - Hubert Comon-Lundh (FoSSaCS, 2004)

Security properties: two agents are sufficient. - Hubert Comon-Lundh; Véronique Cortier (Sci. Comput. Program., 2004)

Normal Attacks on Security Protocols. - Hubert Comon-Lundh (Abstract State Machines, 2005)

The Finite Variant Property: How to Get Rid of Some Algebraic Properties. - Hubert Comon-Lundh; Stéphanie Delaune (RTA, 2005)

Tree automata with one memory set constraints and cryptographic protocols. - Hubert Comon; Véronique Cortier (Theor. Comput. Sci., 2005)

Normal Proofs in Intruder Theories. - Vincent Bernat; Hubert Comon-Lundh (ASIAN, 2006)

Deducibility Constraints, Equational Theory and Electronic Money. - Sergiu Bursuc; Hubert Comon-Lundh; Stéphanie Delaune (Rewriting, Computation and Proof, 2007)

Tree Automata with Memory, Visibility and Structural Constraints. - Hubert Comon-Lundh; Florent Jacquemard; Nicolas Perrin 001 (FoSSaCS, 2007)

Associative-Commutative Deducibility Constraints. - Sergiu Bursuc; Hubert Comon-Lundh; Stéphanie Delaune (STACS, 2007)

Challenges in the Automated Verification of Security Protocols. - Hubert Comon-Lundh (IJCAR, 2008)

Computational soundness of observational equivalence. - Hubert Comon-Lundh; Véronique Cortier (CCS, 2008)

About models of security protocols. - Hubert Comon-Lundh (FSTTCS, 2008)

Visibly Tree Automata with Memory and Constraints. - Hubert Comon-Lundh; Florent Jacquemard; Nicolas Perrin 001 (Log. Methods Comput. Sci., 2008)

Deducibility Constraints. - Sergiu Bursuc; Hubert Comon-Lundh; Stéphanie Delaune (ASIAN, 2009)

Models and Proofs of Protocol Security: A Progress Report. - Martín Abadi; Bruno Blanchet; Hubert Comon-Lundh (CAV, 2009)

Verification of Security Protocols with a Bounded Number of Sessions Based on Resolution for Rigid Variables. - Reynald Affeldt; Hubert Comon-Lundh (Formal to Practical Security, 2009)

Protocol Security and Algebraic Properties: Decision Results for a Bounded Number of Sessions. - Sergiu Bursuc; Hubert Comon-Lundh (RTA, 2009)

Computational and Symbolic Anonymity in an Unbounded Network. - Hubert Comon-Lundh; Yusuke Kawamoto 001; Hideki Sakurada (JSIAM Lett., 2009)

Automating Security Analysis: Symbolic Equivalence of Constraint Systems. - Vincent Cheval; Hubert Comon-Lundh; Stéphanie Delaune (IJCAR, 2010)

Deciding security properties for cryptographic protocols. application to key cycles. - Hubert Comon-Lundh; Véronique Cortier; Eugen Zalinescu (ACM Trans. Comput. Log., 2010)

Constraint solving techniques and enriching the model with equational theories. - Hubert Comon-Lundh; Stéphanie Delaune; Jonathan K. Millen (Formal Models and Techniques for Analyzing Security Protocols, 2011)

Trace equivalence decision: negative tests and non-determinism. - Vincent Cheval; Hubert Comon-Lundh; Stéphanie Delaune (CCS, 2011)

How to prove security of communication protocols? A discussion on the soundness of formal models w.r.t. computational ones. - Hubert Comon-Lundh; Véronique Cortier (STACS, 2011)

Security and Rewriting (Dagstuhl Seminar 11332). - Hubert Comon-Lundh; Ralf Küsters; Catherine Meadows 001 (Dagstuhl Reports, 2011)

Computational Soundness of Indistinguishability Properties without Computable Parsing. - Hubert Comon-Lundh; Masami Hagiya; Yusuke Kawamoto 001; Hideki Sakurada (ISPEC, 2012)

Towards Unconditional Soundness: Computationally Complete Symbolic Attacker. - Gergei Bana; Hubert Comon-Lundh (IACR Cryptol. ePrint Arch., 2012)

Security proof with dishonest keys. - Hubert Comon-Lundh; Véronique Cortier; Guillaume Scerri (IACR Cryptol. ePrint Arch., 2012)

Special Issue on Security and Rewriting Foreword. - Hubert Comon-Lundh; Catherine Meadows 001 (J. Autom. Reason., 2012)

Formal Security Proofs. - Hubert Comon-Lundh; Stéphanie Delaune (Software Safety and Security, 2012)

Tractable Inference Systems: An Extension with a Deducibility Predicate. - Hubert Comon-Lundh; Véronique Cortier; Guillaume Scerri (CADE, 2013)

LICS: Logic in Computer Security - Some Attacker's Models and Related Decision Problems. - Hubert Comon-Lundh (LICS, 2013)

A Computationally Complete Symbolic Attacker for Equivalence Properties. - Gergei Bana; Hubert Comon-Lundh (CCS, 2014)

Deducibility constraints and blind signatures. - Sergiu Bursuc; Hubert Comon-Lundh; Stéphanie Delaune (Inf. Comput., 2014)

Formal Computational Unlinkability Proofs of RFID Protocols. - Hubert Comon; Adrien Koutsos (CSF, 2017)

A procedure for deciding symbolic equivalence between sets of constraint systems. - Vincent Cheval; Hubert Comon-Lundh; Stéphanie Delaune (Inf. Comput., 2017)

Oracle Simulation: A Technique for Protocol Composition with Long Term Shared Secrets. - Hubert Comon; Charlie Jacomme; Guillaume Scerri (CCS, 2020)