Jean-Pierre Jouannaud

According to our database, Jean-Pierre Jouannaud authored at least 91 papers between 1977 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of three.

2024

Drag Rewriting.

Nachum Dershowitz, Jean-Pierre Jouannaud, Fernando Orejas

CoRR, 2024

Confluence of Terminating Rewriting Computations.

Jean-Pierre Jouannaud

Proceedings of the French School of Programming, 2024

2023

Unification of drags and confluence of drag rewriting.

Jean-Pierre Jouannaud, Fernando Orejas

J. Log. Algebraic Methods Program., February, 2023

2022

Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs.

Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, Jiaxiang Liu

Math. Struct. Comput. Sci., August, 2022

2021

Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories.

Gaspard Férey, Jean-Pierre Jouannaud

Proceedings of the PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, 2021

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

Unification of Drags.

Jean-Pierre Jouannaud, Fernando Orejas

Proceedings of the 34th International Workshop on Unification, 2020

2019

Drags: A compositional algebraic framework for graph rewriting.

Nachum Dershowitz, Jean-Pierre Jouannaud

Theor. Comput. Sci., 2019

2018

Graph Path Orderings.

Nachum Dershowitz, Jean-Pierre Jouannaud

Proceedings of the LPAR-22. 22nd International Conference on Logic for Programming, 2018

2017

Coq without Type Casts: A Complete Proof of Coq Modulo Theory.

Jean-Pierre Jouannaud, Pierre-Yves Strub

Proceedings of the LPAR-21, 2017

2015

Normal Higher-Order Termination.

Jean-Pierre Jouannaud, Albert Rubio

ACM Trans. Comput. Log., 2015

The computability path ordering.

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Log. Methods Comput. Sci., 2015

Termination of Dependently Typed Rewrite Rules.

Jean-Pierre Jouannaud, Jianqi Li

Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

Confluence of Layered Rewrite Systems.

Jiaxiang Liu, Jean-Pierre Jouannaud, Mizuhito Ogawa

Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014

Confluence by Critical Pair Analysis.

Jiaxiang Liu, Nachum Dershowitz, Jean-Pierre Jouannaud

Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

Confluence: The Unifying, Expressive Power of Locality.

Jiaxiang Liu, Jean-Pierre Jouannaud

Proceedings of the Specification, Algebra, and Software, 2014

2013

The Blossom of Finite Semantic Trees.

Jean Goubault-Larrecq, Jean-Pierre Jouannaud

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012

From diagrammatic confluence to modularity.

Jean-Pierre Jouannaud, Jiaxiang Liu

Theor. Comput. Sci., 2012

Church-Rosser Properties of Normal Rewriting.

Jean-Pierre Jouannaud, Jianqi Li

Proceedings of the Computer Science Logic (CSL'12), 2012

2011

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

Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

2010

Infinite Families of Finite String Rewriting Systems and Their Confluence.

Jean-Pierre Jouannaud, Benjamin Monate

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

2009

Diagrammatic Confluence and Completion.

Jean-Pierre Jouannaud, Vincent van Oostrom

Proceedings of the Automata, Languages and Programming, 36th Internatilonal Colloquium, 2009

2008

Modular Church-Rosser Modulo: The Complete Picture.

Jean-Pierre Jouannaud, Yoshihito Toyama

Int. J. Softw. Informatics, 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

Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

The Computability Path Ordering: The End of a Quest.

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

2007

Polymorphic higher-order recursive path orderings.

Jean-Pierre Jouannaud, Albert Rubio

J. ACM, 2007

HORPO with Computability Closure: A Reconstruction.

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Proceedings of the Logic for Programming, 2007

Building Decision Procedures in the Calculus of Inductive Constructions.

Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub

Proceedings of the Computer Science Logic, 21st International Workshop, 2007

2006

Preface.

Jean-Pierre Jouannaud, Ian Mackie

Proceedings of the Second International Workshop on Developments in Computational Models, 2006

Joseph Goguen (1941-2006).

Kokichi Futatsugi, Jean-Pierre Jouannaud, José Meseguer

Bull. EATCS, 2006

Higher-Order Orderings for Normal Rewriting.

Jean-Pierre Jouannaud, Albert Rubio

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Modular Church-Rosser Modulo.

Jean-Pierre Jouannaud

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Higher-Order Termination: From Kruskal to Computability.

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio

Proceedings of the Logic for Programming, 2006

From OBJ to ML to Coq.

Jacek Chrzaszcz, Jean-Pierre Jouannaud

Proceedings of the Algebra, Meaning, and Computation, 2006

2005

Automatic Complexity Analysis for Programs Extracted from Coq Proof.

Jean-Pierre Jouannaud, Weiwen Xu

Proceedings of the Workshop on the Constructive Logic for Automated Software Engineering, 2005

Twenty Years Later.

Jean-Pierre Jouannaud

Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

Higher-Order Rewriting: Framework, Confluence and Termination.

Jean-Pierre Jouannaud

Proceedings of the Processes, 2005

2004

Theorem Proving Languages for Verification.

Jean-Pierre Jouannaud

Proceedings of the Automated Technology for Verification and Analysis: Second International Conference, 2004

2002

Inductive-data-type systems.

Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada

Theor. Comput. Sci., 2002

2001

Automata-Driven Automated Induction.

Adel Bouhoula, Jean-Pierre Jouannaud

Inf. Comput., 2001

2000

Specification and proof in membership equational logic.

Adel Bouhoula, Jean-Pierre Jouannaud, José Meseguer

Theor. Comput. Sci., 2000

1999

A Methodological View of Constraint Solving.

Hubert Comon, Mehmet Dincbas, Jean-Pierre Jouannaud, Claude Kirchner

Constraints An Int. J., 1999

The Calculus of algebraic Constructions.

Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada

Proceedings of the Rewriting Techniques and Applications, 10th International Conference, 1999

The Higher-Order Recursive Path Ordering.

Jean-Pierre Jouannaud, Albert Rubio

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

Constraints and Constraint Solving: An Introduction.

Jean-Pierre Jouannaud, Ralf Treinen

Proceedings of the Constraints in Computational Logics: Theory and Applications, 1999

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

Membership equational logic, calculus of inductive instructions, and rewrite logic.

Jean-Pierre Jouannaud

Proceedings of the 1998 International Workshop on Rewriting Logic and its Applications, 1998

1997

Abstract Data Type Systems.

Jean-Pierre Jouannaud, Mitsuhiro Okada

Theor. Comput. Sci., 1997

1996

A Recursive Path Ordering for Higher-Order Terms in <i>eta</i>-Long <i>beta</i>-Normal Form.

Jean-Pierre Jouannaud, Albert Rubio

Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

1995

Problems in Rewriting III.

Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop

Proceedings of the Rewriting Techniques and Applications, 6th International Conference, 1995

1994

Syntacticness, Cycle-Syntacticness, and Shallow Theories

Hubert Comon, Marianne Haberstrau, Jean-Pierre Jouannaud

Inf. Comput., May, 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

Strong Sequentiality of Left-Linear Overlapping Rewrite Systems.

Jean-Pierre Jouannaud, Walid Sadfi

Proceedings of the Conditional and Typed Rewriting Systems, 4th International Workshop, 1994

Modular Termination of Term Rewriting Systems Revisited.

Maribel Fernández, Jean-Pierre Jouannaud

Proceedings of the Recent Trends in Data Type Specification, 10th Workshop on Specification of Abstract Data Types Joint with the 5th COMPASS Workshop, S. Margherita, Italy, May 30, 1994

1993

More Problems in Rewriting.

Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop

Proceedings of the Rewriting Techniques and Applications, 5th International Conference, 1993

Introduction to Rewriting.

Jean-Pierre Jouannaud

Proceedings of the Term Rewriting, 1993

1992

Termination and Completion Modulo Associativity, Commutativity and Identity.

Jean-Pierre Jouannaud, Claude Marché

Theor. Comput. Sci., 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

Decidable Problems in Shallow Equational Theories (Extended Abstract)

Hubert Comon, Marianne Haberstrau, Jean-Pierre Jouannaud

Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), 1992

Rewriting Techniques for Software Engineering.

Jean-Pierre Jouannaud

Proceedings of the Recent Trends in Data Type Specification, 1992

1991

Notations for Rewting.

Nachum Dershowitz, Jean-Pierre Jouannaud

Bull. EATCS, 1991

Executable Higher-Order Algebraic Specifications.

Jean-Pierre Jouannaud

Proceedings of the STACS 91, 1991

Open Problems in Rewriting.

Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop

Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991

A Computation Model for Executable Higher-Order Algebraic Specification Languages

Jean-Pierre Jouannaud, Mitsuhiro Okada

Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991

Satisfiability of Systems of Ordinal Notations with the Subterm Property is Decidable.

Jean-Pierre Jouannaud, Mitsuhiro Okada

Proceedings of the Automata, Languages and Programming, 18th International Colloquium, 1991

Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification.

Jean-Pierre Jouannaud, Claude Kirchner

Proceedings of the Computational Logic - Essays in Honor of Alan Robinson, 1991

1990

Syntactic Theories.

Jean-Pierre Jouannaud

Proceedings of the Mathematical Foundations of Computer Science 1990, 1990

Completion modulo Associativity, Commutativity and Identity (AC1).

Jean-Pierre Jouannaud, Claude Marché

Proceedings of the Design and Implementation of Symbolic Computation Systems, 1990

Tutorial on Rewrite-Based Theorem Proving.

Jieh Hsiang, Jean-Pierre Jouannaud

Proceedings of the 10th International Conference on Automated Deduction, 1990

Rewrite Systems.

Nachum Dershowitz, Jean-Pierre Jouannaud

Proceedings of the Handbook of Theoretical Computer Science, 1990

1989

Automatic Proofs by Induction in Theories without Constructors

Jean-Pierre Jouannaud, Emmanuel Kounalis

Inf. Comput., July, 1989

Unification in Boolean Rings and Abelian Groups.

Alexandre Boudet, Jean-Pierre Jouannaud, Manfred Schmidt-Schauß

J. Symb. Comput., 1989

1988

Unification in Free Extensions of Boolean Rings and Abelian Groups

Alexandre Boudet, Jean-Pierre Jouannaud, Manfred Schmidt-Schauß

Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

OBJ: Programming with Equalities, Subsorts, Overloading and Parameterization.

Jean-Pierre Jouannaud, Claude Kirchner, Hélène Kirchner, Aristide Mégrelis

Proceedings of the Algebraic and Logic Programming, 1988

1987

Reductive conditional term rewriting systems.

Jean-Pierre Jouannaud, B. Waldmann

Proceedings of the Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2/WG 2.2 Working Conference on Formal Description of Programming Concepts, 1987

1986

Completion of a Set of Rules Modulo a Set of Equations.

Jean-Pierre Jouannaud, Hélène Kirchner

SIAM J. Comput., 1986

Automatic Proofs by Induction in Equational Theories Without Constructors

Jean-Pierre Jouannaud, Emmanuel Kounalis

Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

1985

Proofs by induction in equational theories without constructors.

Jean-Pierre Jouannaud, Emmanuel Kounalis

Bull. EATCS, 1985

Principles of OBJ2.

Kokichi Futatsugi, Joseph A. Goguen, Jean-Pierre Jouannaud, José Meseguer

Proceedings of the Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985

Operational Semantics for Order-Sorted Algebra.

Joseph A. Goguen, Jean-Pierre Jouannaud, José Meseguer

Proceedings of the Automata, 1985

1984

Construction D'un Plus Petit Odre de Simplification.

Jean-Pierre Jouannaud, Hélène Kirchner

RAIRO Theor. Informatics Appl., 1984

Termination of a Set of Rules Modulo a Set of Equations.

Jean-Pierre Jouannaud, Miguel Munoz

Proceedings of the 7th International Conference on Automated Deduction, 1984

1983

Church-Rosser Properties of Weakly Terminating Term Rewriting Systems.

Jean-Pierre Jouannaud, Hélène Kirchner, Jean-Luc Rémy

Proceedings of the 8th International Joint Conference on Artificial Intelligence. Karlsruhe, 1983

Incremental Construction of Unification Algorithms in Equational Theories.

Jean-Pierre Jouannaud, Claude Kirchner, Hélène Kirchner

Proceedings of the Automata, 1983

Confluent and Coherent Equational Term Rewriting Systems: Application to Proofs in Abstract Data Types.

Jean-Pierre Jouannaud

Proceedings of the CAAP'83, 1983

Programming and Checking Data Types with REVE.

Jean-Pierre Jouannaud

Proceedings of the Proceedings 2nd Workshop on Abstract Data Type, 1983

1982

On Multiset Orderings.

Jean-Pierre Jouannaud, Pierre Lescanne

Inf. Process. Lett., 1982

Recursive Decomposition Ordering.

Jean-Pierre Jouannaud, Pierre Lescanne, F. Reinig

Proceedings of the Formal Description of Programming Concepts : Proceedings of the IFIP Working Conference on Formal Description of Programming Concepts- II, 1982

1981

Algebraic Manipulations as a Unification and Matching Strategy for Linear Equations in Signed Binary Trees.

Claude Kirchner, Hélène Kirchner, Jean-Pierre Jouannaud

Proceedings of the 7th International Joint Conference on Artificial Intelligence, 1981

1979

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

Proceedings of the Sixth International Joint Conference on Artificial Intelligence, 1979

1977

SISP/1: An Interactive System Able to Synthesize Functions from Examples.

Jean-Pierre Jouannaud, Gérard D. Guiho, Jean-Pierre Treuil

Proceedings of the 5th International Joint Conference on Artificial Intelligence. Cambridge, 1977