| 2008 | LATA | Anti-pattern Matching Modulo. | Claude Kirchner, Radu Kopetz, Pierre-Etienne Moreau |
| 2007 | CCS | Weaving rewrite-based access control policies. | Anderson Santana de Oliveira, Eric Ke Wang, Claude Kirchner, Hlne Kirchner |
| 2007 | ESOP | Anti-pattern Matching. | Claude Kirchner, Radu Kopetz, Pierre-Etienne Moreau |
| 2007 | ESORICS | Modular Access Control Via Strategic Rewriting. | Daniel J. Dougherty, Claude Kirchner, Hlne Kirchner, Anderson Santana de Oliveira |
| 2007 | FOSSACS | The Rewriting Calculus as a Combinatory Reduction System. | Clara Bertolissi, Claude Kirchner |
| 2007 | LFCS | Cut Elimination in Deduction Modulo by Abstract Completion. | Guillaume Burel, Claude Kirchner |
| 2007 | LICS | Principles of Superdeduction. | Paul Brauner, Clment Houtmann, Claude Kirchner |
| 2006 | FOSSACS | On the Confluence of | Frdric Blanqui, Claude Kirchner, Colin Riba |
| 2005 | PPDP | Formal validation of pattern matching code. | Claude Kirchner, Pierre-Etienne Moreau, Antoine Reilles |
| 2003 | CADE | Proof Search and Proof Check for Equational and Inductive Theorems. | Eric Deplagne, Claude Kirchner, Hlne Kirchner, Quang Huy Nguyen |
| 2003 | LICS | Abstract Saturation-Based Inference. | Nachum Dershowitz, Claude Kirchner |
| 2003 | POPL | Pure patterns type systems. | Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori |
| 2002 | AISC | Deduction versus Computation: The Case of Induction. | Eric Deplagne, Claude Kirchner |
| 2002 | LPAR | Binding Logic: Proofs and Models. | Gilles Dowek, Thrse Hardin, Claude Kirchner |
| 2001 | FOSSACS | The Rho Cube. | Horatiu Cirstea, Claude Kirchner, Luigi Liquori |
| 1998 | CP | Generating Feasible Schedules for a Pick-Up and Delivery Problem. | Eric Domenjoud, Claude Kirchner, Jianyang Zhou |
| 1998 | FLOPS | A Functional View of Rewriting and Strategies for a Semantics of ELAN. | Peter Borovansk, Claude Kirchner, Hlne Kirchner |
| 1997 | ICLP | A Modular Framework for the Combination of Unification and Built-In Constraints. | Farid Ajili, Claude Kirchner |
| 1996 | ICLP | Unification via Explicit Substitutions: The Case of Higher-Order Patterns. | Gilles Dowek, Thrse Hardin, Claude Kirchner, Frank Pfenning |
| 1995 | LICS | Higher-Order Unification via Explicit Substitutions (Extended Abstract) | Gilles Dowek, Thrse Hardin, Claude Kirchner |
| 1994 | COMPASS | Sort Inheritance for Order-Sorted Equational Presentations. | Claus Hintermeier, Claude Kirchner, Hlne Kirchner |
| 1994 | ICALP | Dynamically-Typed Computations for Order-Sorted Equational Presentations. | Claus Hintermeier, Claude Kirchner, Hlne Kirchner |
| 1990 | CADE | Tutorial on Equational Unification. | Claude Kirchner |
| 1990 | LICS | Syntactic Theories and Unification | Claude Kirchner, Francis Klay |
| 1989 | ISSAC | Constrained Equational Reasoning. | Claude Kirchner, Hlne Kirchner |
| 1988 | ICALP | Operational Semantics of OBJ-3 (Extended Abstract). | Claude Kirchner, Hlne Kirchner, Jos Meseguer |
| 1987 | LICS | Solving Disequations | Claude Kirchner, Pierre Lescanne |
| 1986 | LICS | Computing Unification Algorithms | Claude Kirchner |
| 1984 | CADE | A New Equational Unification Method: A Generalization of Martelli-Montanari's Algorithm. | Claude Kirchner |
| 1983 | ICALP | Incremental Construction of Unification Algorithms in Equational Theories. | Jean-Pierre Jouannaud, Claude Kirchner, Hlne Kirchner |
| 1981 | IJCAI | Algebraic Manipulations as a Unification and Matching Strategy for Linear Equations in Signed Binary Trees. | Claude Kirchner, Hlne Kirchner, Jean-Pierre Jouannaud |