Jean-Pierre Jouannaud

112 papers A* 16A 4B 11C 1Journal 36Unranked 34
YearRankTypeTitle / Venue / Authors
2025 A conf
Sort-Based Confluence Criteria for Non-Left-Linear Higher-Order Rewriting.
CADE
Thiago Felicissimo, Jean-Pierre Jouannaud
2024 — ch.
Confluence of Terminating Rewriting Computations.
The French School of Programming
Jean-Pierre Jouannaud
2024 J jnl
Drag Rewriting.
CoRR
Nachum Dershowitz, Jean-Pierre Jouannaud, Fernando Orejas
2023 J jnl
Unification of drags and confluence of drag rewriting.
J. Log. Algebraic Methods Program.
Jean-Pierre Jouannaud, Fernando Orejas
2022 J jnl
Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs.
Math. Struct. Comput. Sci.
Gilles Dowek, Gaspard Férey, Jean-Pierre Jouannaud, Jiaxiang Liu
2021 C conf
Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories.
PPDP
Gaspard Férey, Jean-Pierre Jouannaud
2020 J jnl
Corrigendum to "Inductive-data-type systems" [Theoret. Comput. Sci. 272 (1-2) (2002) 41-68].
Theor. Comput. Sci.
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
2020 — conf
Unification of Drags.
UNIF
Jean-Pierre Jouannaud, Fernando Orejas
2019 J jnl
Drags: A compositional algebraic framework for graph rewriting.
Theor. Comput. Sci.
Nachum Dershowitz, Jean-Pierre Jouannaud
2018 B conf
Graph Path Orderings.
LPAR
Nachum Dershowitz, Jean-Pierre Jouannaud
2017 B conf
Coq without Type Casts: A Complete Proof of Coq Modulo Theory.
LPAR
Jean-Pierre Jouannaud, Pierre-Yves Strub
2015 B conf
Confluence of Layered Rewrite Systems.
CSL
Jiaxiang Liu, Jean-Pierre Jouannaud, Mizuhito Ogawa
2015 J jnl
Confluence of Layered Rewrite Systems.
CoRR
Jean-Pierre Jouannaud, Jiaxiang Liu, Mizuhito Ogawa
2015 J jnl
Normal Higher-Order Termination.
ACM Trans. Comput. Log.
Jean-Pierre Jouannaud, Albert Rubio
2015 — conf
Termination of Dependently Typed Rewrite Rules.
TLCA
Jean-Pierre Jouannaud, Jianqi Li
2015 J jnl
The computability path ordering.
Log. Methods Comput. Sci.
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
2014 — conf
Confluence by Critical Pair Analysis.
RTA-TLCA
Jiaxiang Liu, Nachum Dershowitz, Jean-Pierre Jouannaud
2014 — conf
Confluence: The Unifying, Expressive Power of Locality.
Specification, Algebra, and Software
Jiaxiang Liu, Jean-Pierre Jouannaud
2013 — conf
The Blossom of Finite Semantic Trees.
Programming Logics
Jean Goubault-Larrecq, Jean-Pierre Jouannaud
2012 B conf
Church-Rosser Properties of Normal Rewriting.
CSL
Jean-Pierre Jouannaud, Jianqi Li
2012 J jnl
From diagrammatic confluence to modularity.
Theor. Comput. Sci.
Jean-Pierre Jouannaud, Jiaxiang Liu
2011 B ed.
Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings
CPP
Jean-Pierre Jouannaud, Zhong Shao
2011 A* conf
CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory.
LICS
Bruno Barras, Jean-Pierre Jouannaud, Pierre-Yves Strub, Qian Wang
2010 — conf
Infinite Families of Finite String Rewriting Systems and Their Confluence.
LPAR (Yogyakarta)
Jean-Pierre Jouannaud, Benjamin Monate
2009 — conf
Diagrammatic Confluence and Completion.
ICALP (2)
Jean-Pierre Jouannaud, Vincent van Oostrom
2008 — conf
From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures.
IFIP TCS
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
2008 J jnl
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures
CoRR
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
2008 J jnl
Modular Church-Rosser Modulo: The Complete Picture.
Int. J. Softw. Informatics
Jean-Pierre Jouannaud, Yoshihito Toyama
2008 B conf
The Computability Path Ordering: The End of a Quest.
CSL
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
2008 J jnl
The computability path ordering: the end of a quest
CoRR
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
2007 J jnl
Building Decision Procedures in the Calculus of Inductive Constructions
CoRR
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
2007 B conf
Building Decision Procedures in the Calculus of Inductive Constructions.
CSL
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
2007 J jnl
HORPO with Computability Closure : A Reconstruction
CoRR
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
2007 B conf
HORPO with Computability Closure: A Reconstruction.
LPAR
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
2007 J jnl
Polymorphic higher-order recursive path orderings.
J. ACM
Jean-Pierre Jouannaud, Albert Rubio
2007 — ed.
Proceedings of the Second International Workshop on Developments in Computational Models, DCM@ICALP 2006, Venice, Italy, July 16, 2006
DCM@ICALP
Jean-Pierre Jouannaud, Ian Mackie
2006 — ed.
Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday
Essays Dedicated to Joseph A. Goguen
Kokichi Futatsugi, Jean-Pierre Jouannaud, José Meseguer
2006 — conf
From OBJ to ML to Coq.
Essays Dedicated to Joseph A. Goguen
Jacek Chrzaszcz, Jean-Pierre Jouannaud
2006 — conf
Higher-Order Orderings for Normal Rewriting.
RTA
Jean-Pierre Jouannaud, Albert Rubio
2006 B conf
Higher-Order Termination: From Kruskal to Computability.
LPAR
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
2006 J jnl
Higher-Order Termination: from Kruskal to Computability
CoRR
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
2006 J jnl
Inductive-data-type Systems
CoRR
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
2006 J jnl
Joseph Goguen (1941-2006).
Bull. EATCS
Kokichi Futatsugi, Jean-Pierre Jouannaud, José Meseguer
2006 — conf
Modular Church-Rosser Modulo.
RTA
Jean-Pierre Jouannaud
2006 — conf
Preface.
DCM@ICALP
Jean-Pierre Jouannaud, Ian Mackie
2006 J jnl
The Calculus of Algebraic Constructions
CoRR
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
2005 — conf
Automatic Complexity Analysis for Programs Extracted from Coq Proof.
CLASE
Jean-Pierre Jouannaud, Weiwen Xu
2005 — conf
Higher-Order Rewriting: Framework, Confluence and Termination.
Processes, Terms and Cycles
Jean-Pierre Jouannaud
2005 — conf
Twenty Years Later.
RTA
Jean-Pierre Jouannaud
2004 B conf
Theorem Proving Languages for Verification.
ATVA
Jean-Pierre Jouannaud
2002 J jnl
Inductive-data-type systems.
Theor. Comput. Sci.
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
2001 J jnl
Automata-Driven Automated Induction.
Inf. Comput.
Adel Bouhoula, Jean-Pierre Jouannaud
2000 J jnl
Specification and proof in membership equational logic.
Theor. Comput. Sci.
Adel Bouhoula, Jean-Pierre Jouannaud, José Meseguer
1999 J jnl
A Methodological View of Constraint Solving.
Constraints An Int. J.
Hubert Comon, Mehmet Dincbas, Jean-Pierre Jouannaud, Claude Kirchner
1999 — conf
Constraints and Constraint Solving: An Introduction.
CCL
Jean-Pierre Jouannaud, Ralf Treinen
1999 — conf
The Calculus of algebraic Constructions.
RTA
Frédéric Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
1999 A* conf
The Higher-Order Recursive Path Ordering.
LICS
Jean-Pierre Jouannaud, Albert Rubio
1998 — conf
Membership equational logic, calculus of inductive instructions, and rewrite logic.
WRLA
Jean-Pierre Jouannaud
1998 J jnl
Rewrite Orderings for Higher-Order Terms in eta-Long beta-Normal Form and Recursive Path Ordering.
Theor. Comput. Sci.
Jean-Pierre Jouannaud, Albert Rubio
1997 J jnl
Abstract Data Type Systems.
Theor. Comput. Sci.
Jean-Pierre Jouannaud, Mitsuhiro Okada
1997 A* conf
Automata-Driven Automated Induction.
LICS
Adel Bouhoula, Jean-Pierre Jouannaud
1997 — conf
Specification and Proof in Membership Equational Logic.
TAPSOFT
Adel Bouhoula, Jean-Pierre Jouannaud, José Meseguer
1996 — conf
A Recursive Path Ordering for Higher-Order Terms in
RTA
Jean-Pierre Jouannaud, Albert Rubio
1995 — conf
Problems in Rewriting III.
RTA
Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop
1995 — ed.
Term Rewriting, French Spring School of Theoretical Computer Science, Font Romeux, France, May 17-21, 1993, Advanced Course
Term Rewriting
Hubert Comon, Jean-Pierre Jouannaud
1994 J jnl
Book Review: A Proof Theory for General Unification. By Wayne Snyder. (Birkhauser, 1991. vi+175 pages. ISBN 0-8176-3593-9. $28.00).
SIGACT News
Jean-Pierre Jouannaud
1994 — ed.
Constraints in Computational Logics, First International Conference, CCL'94, Munich, Germany, September 7-9, 1994
CCL
Jean-Pierre Jouannaud
1994 — conf
Modular Termination of Term Rewriting Systems Revisited.
COMPASS/ADT
Maribel Fernández, Jean-Pierre Jouannaud
1994 — conf
Strong Sequentiality of Left-Linear Overlapping Rewrite Systems.
CTRS
Jean-Pierre Jouannaud, Walid Sadfi
1994 J jnl
Syntacticness, Cycle-Syntacticness, and Shallow Theories
Inf. Comput.
Hubert Comon, Marianne Haberstrau, Jean-Pierre Jouannaud
1993 — conf
Introduction to Rewriting.
Term Rewriting
Jean-Pierre Jouannaud
1993 — conf
More Problems in Rewriting.
RTA
Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop
1993 — ed.
TAPSOFT'93: Theory and Practice of Software Development, International Joint Conference CAAP/FASE, Orsay, France, April 13-17, 1993, Proceedings
TAPSOFT
Marie-Claude Gaudel, Jean-Pierre Jouannaud
1992 A* conf
Decidable Problems in Shallow Equational Theories (Extended Abstract)
LICS
Hubert Comon, Marianne Haberstrau, Jean-Pierre Jouannaud
1992 J jnl
Programming with Equalitiers, Subsorts, Overloading and Parametrization in OBJ.
J. Log. Program.
Jean-Pierre Jouannaud, Claude Kirchner, Hélène Kirchner, Aristide Mégrelis
1992 — conf
Rewriting Techniques for Software Engineering.
COMPASS/ADT
Jean-Pierre Jouannaud
1992 J jnl
Termination and Completion Modulo Associativity, Commutativity and Identity.
Theor. Comput. Sci.
Jean-Pierre Jouannaud, Claude Marché
1991 A* conf
A Computation Model for Executable Higher-Order Algebraic Specification Languages
LICS
Jean-Pierre Jouannaud, Mitsuhiro Okada
1991 A conf
Executable Higher-Order Algebraic Specifications.
STACS
Jean-Pierre Jouannaud
1991 J jnl
Notations for Rewting.
Bull. EATCS
Nachum Dershowitz, Jean-Pierre Jouannaud
1991 — conf
Open Problems in Rewriting.
RTA
Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop
1991 A* conf
Satisfiability of Systems of Ordinal Notations with the Subterm Property is Decidable.
ICALP
Jean-Pierre Jouannaud, Mitsuhiro Okada
1991 — conf
Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification.
Computational Logic - Essays in Honor of Alan Robinson
Jean-Pierre Jouannaud, Claude Kirchner
1990 — conf
Completion modulo Associativity, Commutativity and Identity (AC1).
DISCO
Jean-Pierre Jouannaud, Claude Marché
1990 — ch.
Rewrite Systems.
Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B)
Nachum Dershowitz, Jean-Pierre Jouannaud
1990 B conf
Syntactic Theories.
MFCS
Jean-Pierre Jouannaud
1990 A conf
Tutorial on Rewrite-Based Theorem Proving.
CADE
Jieh Hsiang, Jean-Pierre Jouannaud
1989 J jnl
Automatic Proofs by Induction in Theories without Constructors
Inf. Comput.
Jean-Pierre Jouannaud, Emmanuel Kounalis
1989 J jnl
Unification in Boolean Rings and Abelian Groups.
J. Symb. Comput.
Alexandre Boudet, Jean-Pierre Jouannaud, Manfred Schmidt-Schauß
1988 — ed.
Conditional Term Rewriting Systems, 1st International Workshop, Orsay, France, July 8-10, 1987, Proceedings
CTRS
Stéphane Kaplan, Jean-Pierre Jouannaud
1988 — conf
OBJ: Programming with Equalities, Subsorts, Overloading and Parameterization.
ALP
Jean-Pierre Jouannaud, Claude Kirchner, Hélène Kirchner, Aristide Mégrelis
1988 A* conf
Unification in Free Extensions of Boolean Rings and Abelian Groups
LICS
Alexandre Boudet, Jean-Pierre Jouannaud, Manfred Schmidt-Schauß
1987 — conf
Reductive conditional term rewriting systems.
Formal Description of Programming Concepts
Jean-Pierre Jouannaud, B. Waldmann
1986 A* conf
Automatic Proofs by Induction in Equational Theories Without Constructors
LICS
Jean-Pierre Jouannaud, Emmanuel Kounalis
1986 J jnl
Completion of a Set of Rules Modulo a Set of Equations.
SIAM J. Comput.
Jean-Pierre Jouannaud, Hélène Kirchner
1985 — ed.
Functional Programming Languages and Computer Architecture, FPCA 1985, Nancy, France, September 16-19, 1985, Proceedings
FPCA
Jean-Pierre Jouannaud
1985 A* conf
Operational Semantics for Order-Sorted Algebra.
ICALP
Joseph A. Goguen, Jean-Pierre Jouannaud, José Meseguer
1985 A* conf
Principles of OBJ2.
POPL
Kokichi Futatsugi, Joseph A. Goguen, Jean-Pierre Jouannaud, José Meseguer
1985 J jnl
Proofs by induction in equational theories without constructors.
Bull. EATCS
Jean-Pierre Jouannaud, Emmanuel Kounalis
1985 — ed.
Rewriting Techniques and Applications, First International Conference, RTA-85, Dijon, France, May 20-22, 1985, Proceedings
RTA
Jean-Pierre Jouannaud
1984 A* conf
Completion of a Set of Rules Modulo a Set of Equations.
POPL
Jean-Pierre Jouannaud, Hélène Kirchner
1984 J jnl
Construction D'un Plus Petit Odre de Simplification.
RAIRO Theor. Informatics Appl.
Jean-Pierre Jouannaud, Hélène Kirchner
1984 A conf
Termination of a Set of Rules Modulo a Set of Equations.
CADE
Jean-Pierre Jouannaud, Miguel Munoz
1983 A* conf
Church-Rosser Properties of Weakly Terminating Term Rewriting Systems.
IJCAI
Jean-Pierre Jouannaud, Hélène Kirchner, Jean-Luc Rémy
1983 — conf
Confluent and Coherent Equational Term Rewriting Systems: Application to Proofs in Abstract Data Types.
CAAP
Jean-Pierre Jouannaud
1983 A* conf
Incremental Construction of Unification Algorithms in Equational Theories.
ICALP
Jean-Pierre Jouannaud, Claude Kirchner, Hélène Kirchner
1983 — conf
Programming and Checking Data Types with REVE.
ADT
Jean-Pierre Jouannaud
1982 J jnl
On Multiset Orderings.
Inf. Process. Lett.
Jean-Pierre Jouannaud, Pierre Lescanne
1982 — conf
Recursive Decomposition Ordering.
Formal Description of Programming Concepts
Jean-Pierre Jouannaud, Pierre Lescanne, F. Reinig
1981 A* conf
Algebraic Manipulations as a Unification and Matching Strategy for Linear Equations in Signed Binary Trees.
IJCAI
Claude Kirchner, Hélène Kirchner, Jean-Pierre Jouannaud
1979 A* conf
Characterization of a Class of Functions Synthesized from Examples by a SUMMERS Like Method Using a "B.M.W." Matching Technique.
IJCAI
Jean-Pierre Jouannaud, Yves Kodratoff
1977 A* conf
SISP/1: An Interactive System Able to Synthesize Functions from Examples.
IJCAI
Jean-Pierre Jouannaud, Gérard D. Guiho, Jean-Pierre Treuil