| 2025 | CADE | Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting. | Thiago Felicissimo, Jean-Pierre Jouannaud |
| 2021 | PPDP | Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories. | Gaspard Frey, Jean-Pierre Jouannaud |
| 2018 | LPAR | Graph Path Orderings. | Nachum Dershowitz, Jean-Pierre Jouannaud |
| 2017 | LPAR | Coq without Type Casts: A Complete Proof of Coq Modulo Theory. | Jean-Pierre Jouannaud, Pierre-Yves Strub |
| 2015 | CSL | Confluence of Layered Rewrite Systems. | Jiaxiang Liu, Jean-Pierre Jouannaud, Mizuhito Ogawa |
| 2012 | CSL | Church-Rosser Properties of Normal Rewriting. | Jean-Pierre Jouannaud, Jianqi Li |
| 2011 | LICS | CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory. | Bruno Barras, Jean-Pierre Jouannaud, Pierre-Yves Strub, Qian Wang |
| 2010 | LPAR | Infinite Families of Finite String Rewriting Systems and Their Confluence. | Jean-Pierre Jouannaud, Benjamin Monate |
| 2009 | ICALP | Diagrammatic Confluence and Completion. | Jean-Pierre Jouannaud, Vincent van Oostrom |
| 2008 | CSL | The Computability Path Ordering: The End of a Quest. | Frdric Blanqui, Jean-Pierre Jouannaud, Albert Rubio |
| 2007 | CSL | Building Decision Procedures in the Calculus of Inductive Constructions. | Frdric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub |
| 2007 | LPAR | HORPO with Computability Closure: A Reconstruction. | Frdric Blanqui, Jean-Pierre Jouannaud, Albert Rubio |
| 2006 | LPAR | Higher-Order Termination: From Kruskal to Computability. | Frdric Blanqui, Jean-Pierre Jouannaud, Albert Rubio |
| 2004 | ATVA | Theorem Proving Languages for Verification. | Jean-Pierre Jouannaud |
| 1999 | LICS | The Higher-Order Recursive Path Ordering. | Jean-Pierre Jouannaud, Albert Rubio |
| 1997 | LICS | Automata-Driven Automated Induction. | Adel Bouhoula, Jean-Pierre Jouannaud |
| 1994 | COMPASS | Modular Termination of Term Rewriting Systems Revisited. | Maribel Fernndez, Jean-Pierre Jouannaud |
| 1992 | COMPASS | Rewriting Techniques for Software Engineering. | Jean-Pierre Jouannaud |
| 1992 | LICS | Decidable Problems in Shallow Equational Theories (Extended Abstract) | Hubert Comon, Marianne Haberstrau, Jean-Pierre Jouannaud |
| 1991 | ICALP | Satisfiability of Systems of Ordinal Notations with the Subterm Property is Decidable. | Jean-Pierre Jouannaud, Mitsuhiro Okada |
| 1991 | LICS | A Computation Model for Executable Higher-Order Algebraic Specification Languages | Jean-Pierre Jouannaud, Mitsuhiro Okada |
| 1991 | STACS | Executable Higher-Order Algebraic Specifications. | Jean-Pierre Jouannaud |
| 1990 | CADE | Tutorial on Rewrite-Based Theorem Proving. | Jieh Hsiang, Jean-Pierre Jouannaud |
| 1990 | MFCS | Syntactic Theories. | Jean-Pierre Jouannaud |
| 1988 | LICS | Unification in Free Extensions of Boolean Rings and Abelian Groups | Alexandre Boudet, Jean-Pierre Jouannaud, Manfred Schmidt-Schau |
| 1986 | LICS | Automatic Proofs by Induction in Equational Theories Without Constructors | Jean-Pierre Jouannaud, Emmanuel Kounalis |
| 1985 | ICALP | Operational Semantics for Order-Sorted Algebra. | Joseph A. Goguen, Jean-Pierre Jouannaud, Jos Meseguer |
| 1985 | POPL | Principles of OBJ2. | Kokichi Futatsugi, Joseph A. Goguen, Jean-Pierre Jouannaud, Jos Meseguer |
| 1984 | CADE | Termination of a Set of Rules Modulo a Set of Equations. | Jean-Pierre Jouannaud, Miguel Munoz |
| 1984 | POPL | Completion of a Set of Rules Modulo a Set of Equations. | Jean-Pierre Jouannaud, Hlne Kirchner |
| 1983 | ICALP | Incremental Construction of Unification Algorithms in Equational Theories. | Jean-Pierre Jouannaud, Claude Kirchner, Hlne Kirchner |
| 1983 | IJCAI | Church-Rosser Properties of Weakly Terminating Term Rewriting Systems. | Jean-Pierre Jouannaud, Hlne Kirchner, Jean-Luc Rmy |
| 1981 | IJCAI | Algebraic Manipulations as a Unification and Matching Strategy for Linear Equations in Signed Binary Trees. | Claude Kirchner, Hlne Kirchner, Jean-Pierre Jouannaud |
| 1979 | IJCAI | Characterization of a Class of Functions Synthesized from Examples by a SUMMERS Like Method Using a "B.M.W." Matching Technique. | Jean-Pierre Jouannaud, Yves Kodratoff |
| 1977 | IJCAI | SISP/1: An Interactive System Able to Synthesize Functions from Examples. | Jean-Pierre Jouannaud, Grard D. Guiho, Jean-Pierre Treuil |