SISP/1: An Interactive System Able to Synthesize Functions from Examples. - Jean-Pierre Jouannaud; Gérard D. Guiho; Jean-Pierre Treuil (IJCAI, 1977)

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 (IJCAI, 1979)

Algebraic Manipulations as a Unification and Matching Strategy for Linear Equations in Signed Binary Trees. - Claude Kirchner; Hélène Kirchner; Jean-Pierre Jouannaud (IJCAI, 1981)

Recursive Decomposition Ordering. - Jean-Pierre Jouannaud; Pierre Lescanne; F. Reinig (Formal Description of Programming Concepts, 1982)

On Multiset Orderings. - Jean-Pierre Jouannaud; Pierre Lescanne (Inf. Process. Lett., 1982)

Programming and Checking Data Types with REVE. - Jean-Pierre Jouannaud (ADT, 1983)

Confluent and Coherent Equational Term Rewriting Systems: Application to Proofs in Abstract Data Types. - Jean-Pierre Jouannaud (CAAP, 1983)

Incremental Construction of Unification Algorithms in Equational Theories. - Jean-Pierre Jouannaud; Claude Kirchner; Hélène Kirchner (ICALP, 1983)

Church-Rosser Properties of Weakly Terminating Term Rewriting Systems. - Jean-Pierre Jouannaud; Hélène Kirchner; Jean-Luc Rémy (IJCAI, 1983)

Termination of a Set of Rules Modulo a Set of Equations. - Jean-Pierre Jouannaud; Miguel Munoz (CADE, 1984)

Construction D'un Plus Petit Odre de Simplification. - Jean-Pierre Jouannaud; Hélène Kirchner (RAIRO Theor. Informatics Appl., 1984)

Operational Semantics for Order-Sorted Algebra. - Joseph A. Goguen; Jean-Pierre Jouannaud; José Meseguer 001 (ICALP, 1985)

Principles of OBJ2. - Kokichi Futatsugi; Joseph A. Goguen; Jean-Pierre Jouannaud; José Meseguer 001 (POPL, 1985)

Proofs by induction in equational theories without constructors. - Jean-Pierre Jouannaud; Emmanuel Kounalis (Bull. EATCS, 1985)

Automatic Proofs by Induction in Equational Theories Without Constructors - Jean-Pierre Jouannaud; Emmanuel Kounalis (LICS, 1986)

Completion of a Set of Rules Modulo a Set of Equations. - Jean-Pierre Jouannaud; Hélène Kirchner (SIAM J. Comput., 1986)

Reductive conditional term rewriting systems. - Jean-Pierre Jouannaud; B. Waldmann (Formal Description of Programming Concepts, 1987)

OBJ: Programming with Equalities, Subsorts, Overloading and Parameterization. - Jean-Pierre Jouannaud; Claude Kirchner; Hélène Kirchner; Aristide Mégrelis (ALP, 1988)

Unification in Free Extensions of Boolean Rings and Abelian Groups - Alexandre Boudet; Jean-Pierre Jouannaud; Manfred Schmidt-Schauß (LICS, 1988)

Unification in Boolean Rings and Abelian Groups. - Alexandre Boudet; Jean-Pierre Jouannaud; Manfred Schmidt-Schauß (J. Symb. Comput., 1989)

Automatic Proofs by Induction in Theories without Constructors - Jean-Pierre Jouannaud; Emmanuel Kounalis (Inf. Comput., 1989)

Rewrite Systems. - Nachum Dershowitz; Jean-Pierre Jouannaud (Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), 1990)

Tutorial on Rewrite-Based Theorem Proving. - Jieh Hsiang; Jean-Pierre Jouannaud (CADE, 1990)

Completion modulo Associativity, Commutativity and Identity (AC1). - Jean-Pierre Jouannaud; Claude Marché (DISCO, 1990)

Syntactic Theories. - Jean-Pierre Jouannaud (MFCS, 1990)

Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification. - Jean-Pierre Jouannaud; Claude Kirchner (Computational Logic - Essays in Honor of Alan Robinson, 1991)

Satisfiability of Systems of Ordinal Notations with the Subterm Property is Decidable. - Jean-Pierre Jouannaud; Mitsuhiro Okada (ICALP, 1991)

A Computation Model for Executable Higher-Order Algebraic Specification Languages - Jean-Pierre Jouannaud; Mitsuhiro Okada (LICS, 1991)

Open Problems in Rewriting. - Nachum Dershowitz; Jean-Pierre Jouannaud; Jan Willem Klop (RTA, 1991)

Executable Higher-Order Algebraic Specifications. - Jean-Pierre Jouannaud (STACS, 1991)

Notations for Rewting. - Nachum Dershowitz; Jean-Pierre Jouannaud (Bull. EATCS, 1991)

Rewriting Techniques for Software Engineering. - Jean-Pierre Jouannaud (COMPASS/ADT, 1992)

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

Programming with Equalitiers, Subsorts, Overloading and Parametrization in OBJ. - Jean-Pierre Jouannaud; Claude Kirchner; Hélène Kirchner; Aristide Mégrelis (J. Log. Program., 1992)

Termination and Completion Modulo Associativity, Commutativity and Identity. - Jean-Pierre Jouannaud; Claude Marché (Theor. Comput. Sci., 1992)

Introduction to Rewriting. - Jean-Pierre Jouannaud (Term Rewriting, 1993)

More Problems in Rewriting. - Nachum Dershowitz; Jean-Pierre Jouannaud; Jan Willem Klop (RTA, 1993)

Modular Termination of Term Rewriting Systems Revisited. - Maribel Fernández; Jean-Pierre Jouannaud (COMPASS/ADT, 1994)

Strong Sequentiality of Left-Linear Overlapping Rewrite Systems. - Jean-Pierre Jouannaud; Walid Sadfi (CTRS, 1994)

Book Review: A Proof Theory for General Unification. By Wayne Snyder. (Birkhauser, 1991. vi+175 pages. ISBN 0-8176-3593-9. $28.00). - Jean-Pierre Jouannaud (SIGACT News, 1994)

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

Problems in Rewriting III. - Nachum Dershowitz; Jean-Pierre Jouannaud; Jan Willem Klop (RTA, 1995)

A Recursive Path Ordering for Higher-Order Terms in eta-Long beta-Normal Form. - Jean-Pierre Jouannaud; Albert Rubio (RTA, 1996)

Abstract Data Type Systems. - Jean-Pierre Jouannaud; Mitsuhiro Okada (Theor. Comput. Sci., 1997)

Membership equational logic, calculus of inductive instructions, and rewrite logic. - Jean-Pierre Jouannaud (WRLA, 1998)

Rewrite Orderings for Higher-Order Terms in eta-Long beta-Normal Form and Recursive Path Ordering. - Jean-Pierre Jouannaud; Albert Rubio (Theor. Comput. Sci., 1998)

Constraints and Constraint Solving: An Introduction. - Jean-Pierre Jouannaud; Ralf Treinen (CCL, 1999)

The Higher-Order Recursive Path Ordering. - Jean-Pierre Jouannaud; Albert Rubio (LICS, 1999)

The Calculus of algebraic Constructions. - Frédéric Blanqui; Jean-Pierre Jouannaud; Mitsuhiro Okada (RTA, 1999)

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

Specification and proof in membership equational logic. - Adel Bouhoula; Jean-Pierre Jouannaud; José Meseguer 001 (Theor. Comput. Sci., 2000)

Automata-Driven Automated Induction. - Adel Bouhoula; Jean-Pierre Jouannaud (Inf. Comput., 2001)

Inductive-data-type systems. - Frédéric Blanqui; Jean-Pierre Jouannaud; Mitsuhiro Okada (Theor. Comput. Sci., 2002)

Theorem Proving Languages for Verification. - Jean-Pierre Jouannaud (ATVA, 2004)

Higher-Order Rewriting: Framework, Confluence and Termination. - Jean-Pierre Jouannaud (Processes, Terms and Cycles, 2005)

Twenty Years Later. - Jean-Pierre Jouannaud (RTA, 2005)

Automatic Complexity Analysis for Programs Extracted from Coq Proof. - Jean-Pierre Jouannaud; Weiwen Xu (CLASE, 2005)

From OBJ to ML to Coq. - Jacek Chrzaszcz; Jean-Pierre Jouannaud (Essays Dedicated to Joseph A. Goguen, 2006)

Higher-Order Termination: From Kruskal to Computability. - Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio (LPAR, 2006)

Modular Church-Rosser Modulo. - Jean-Pierre Jouannaud (RTA, 2006)

Higher-Order Orderings for Normal Rewriting. - Jean-Pierre Jouannaud; Albert Rubio (RTA, 2006)

Joseph Goguen (1941-2006). - Kokichi Futatsugi; Jean-Pierre Jouannaud; José Meseguer 001 (Bull. EATCS, 2006)

Preface. - Jean-Pierre Jouannaud; Ian Mackie (DCM@ICALP, 2006)

Building Decision Procedures in the Calculus of Inductive Constructions. - Frédéric Blanqui; Jean-Pierre Jouannaud; Pierre-Yves Strub (CSL, 2007)

HORPO with Computability Closure: A Reconstruction. - Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio (LPAR, 2007)

Polymorphic higher-order recursive path orderings. - Jean-Pierre Jouannaud; Albert Rubio (J. ACM, 2007)

The Computability Path Ordering: The End of a Quest. - Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio (CSL, 2008)

From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures. - Frédéric Blanqui; Jean-Pierre Jouannaud; Pierre-Yves Strub (IFIP TCS, 2008)

Modular Church-Rosser Modulo: The Complete Picture. - Jean-Pierre Jouannaud; Yoshihito Toyama (Int. J. Softw. Informatics, 2008)

Diagrammatic Confluence and Completion. - Jean-Pierre Jouannaud; Vincent van Oostrom (ICALP (2), 2009)

Infinite Families of Finite String Rewriting Systems and Their Confluence. - Jean-Pierre Jouannaud; Benjamin Monate (LPAR (Yogyakarta), 2010)

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 (LICS, 2011)

Church-Rosser Properties of Normal Rewriting. - Jean-Pierre Jouannaud; Jianqi Li (CSL, 2012)

From diagrammatic confluence to modularity. - Jean-Pierre Jouannaud; Jiaxiang Liu 001 (Theor. Comput. Sci., 2012)

The Blossom of Finite Semantic Trees. - Jean Goubault-Larrecq; Jean-Pierre Jouannaud (Programming Logics, 2013)

Confluence: The Unifying, Expressive Power of Locality. - Jiaxiang Liu 001; Jean-Pierre Jouannaud (Specification, Algebra, and Software, 2014)

Confluence by Critical Pair Analysis. - Jiaxiang Liu 001; Nachum Dershowitz; Jean-Pierre Jouannaud (RTA-TLCA, 2014)

Confluence of Layered Rewrite Systems. - Jiaxiang Liu 001; Jean-Pierre Jouannaud; Mizuhito Ogawa (CSL, 2015)

Termination of Dependently Typed Rewrite Rules. - Jean-Pierre Jouannaud; Jianqi Li (TLCA, 2015)

The computability path ordering. - Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio (Log. Methods Comput. Sci., 2015)

Normal Higher-Order Termination. - Jean-Pierre Jouannaud; Albert Rubio (ACM Trans. Comput. Log., 2015)

Coq without Type Casts: A Complete Proof of Coq Modulo Theory. - Jean-Pierre Jouannaud; Pierre-Yves Strub (LPAR, 2017)

Graph Path Orderings. - Nachum Dershowitz; Jean-Pierre Jouannaud (LPAR, 2018)

Drags: A compositional algebraic framework for graph rewriting. - Nachum Dershowitz; Jean-Pierre Jouannaud (Theor. Comput. Sci., 2019)

Unification of Drags. - Jean-Pierre Jouannaud; Fernando Orejas (UNIF, 2020)

Corrigendum to "Inductive-data-type systems" [Theoret. Comput. Sci. 272 (1-2) (2002) 41-68]. - Frédéric Blanqui; Jean-Pierre Jouannaud; Mitsuhiro Okada (Theor. Comput. Sci., 2020)

Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories. - Gaspard Férey; Jean-Pierre Jouannaud (PPDP, 2021)

Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs. - Gilles Dowek; Gaspard Férey; Jean-Pierre Jouannaud; Jiaxiang Liu 001 (Math. Struct. Comput. Sci., 2022)

Unification of drags and confluence of drag rewriting. - Jean-Pierre Jouannaud; Fernando Orejas (J. Log. Algebraic Methods Program., 2023)

Confluence of Terminating Rewriting Computations. - Jean-Pierre Jouannaud (The French School of Programming, 2024)

Drag Rewriting. - Nachum Dershowitz; Jean-Pierre Jouannaud; Fernando Orejas (CoRR, 2024)

Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting. - Thiago Felicissimo; Jean-Pierre Jouannaud (CADE, 2025)