Jean-Pierre Jouannaud

Orcid: 0000-0003-4790-9927

Affiliations:
  • École Polytechnique, Paris, France


According to our database1, Jean-Pierre Jouannaud authored at least 89 papers between 1977 and 2023.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2023
Unification of drags and confluence of drag rewriting.
J. Log. Algebraic Methods Program., February, 2023

2022
Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs.
Math. Struct. Comput. Sci., August, 2022

2021
Confluence in Non-Left-Linear Untyped Higher-Order Rewrite Theories.
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].
Theor. Comput. Sci., 2020

Unification of Drags.
Proceedings of the 34th International Workshop on Unification, 2020

2019
Drags: A compositional algebraic framework for graph rewriting.
Theor. Comput. Sci., 2019

2018
Graph Path Orderings.
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.
Proceedings of the LPAR-21, 2017

2015
Normal Higher-Order Termination.
ACM Trans. Comput. Log., 2015

The computability path ordering.
Log. Methods Comput. Sci., 2015

Termination of Dependently Typed Rewrite Rules.
Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications, 2015

Confluence of Layered Rewrite Systems.
Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014
Confluence by Critical Pair Analysis.
Proceedings of the Rewriting and Typed Lambda Calculi - Joint International Conference, 2014

Confluence: The Unifying, Expressive Power of Locality.
Proceedings of the Specification, Algebra, and Software, 2014

2013
The Blossom of Finite Semantic Trees.
Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012
From diagrammatic confluence to modularity.
Theor. Comput. Sci., 2012

Church-Rosser Properties of Normal Rewriting.
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.
Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

2010
Infinite Families of Finite String Rewriting Systems and Their Confluence.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

2009
Diagrammatic Confluence and Completion.
Proceedings of the Automata, Languages and Programming, 36th Internatilonal Colloquium, 2009

2008
Modular Church-Rosser Modulo: The Complete Picture.
Int. J. Softw. Informatics, 2008

From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures.
Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

The Computability Path Ordering: The End of a Quest.
Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

2007
Polymorphic higher-order recursive path orderings.
J. ACM, 2007

HORPO with Computability Closure: A Reconstruction.
Proceedings of the Logic for Programming, 2007

Building Decision Procedures in the Calculus of Inductive Constructions.
Proceedings of the Computer Science Logic, 21st International Workshop, 2007

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

Joseph Goguen (1941-2006).
Bull. EATCS, 2006

Higher-Order Orderings for Normal Rewriting.
Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Modular Church-Rosser Modulo.
Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

Higher-Order Termination: From Kruskal to Computability.
Proceedings of the Logic for Programming, 2006

From OBJ to ML to Coq.
Proceedings of the Algebra, Meaning, and Computation, 2006

2005
Automatic Complexity Analysis for Programs Extracted from Coq Proof.
Proceedings of the Workshop on the Constructive Logic for Automated Software Engineering, 2005

Twenty Years Later.
Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

Higher-Order Rewriting: Framework, Confluence and Termination.
Proceedings of the Processes, 2005

2004
Theorem Proving Languages for Verification.
Proceedings of the Automated Technology for Verification and Analysis: Second International Conference, 2004

2002
Inductive-data-type systems.
Theor. Comput. Sci., 2002

2001
Automata-Driven Automated Induction.
Inf. Comput., 2001

2000
Specification and proof in membership equational logic.
Theor. Comput. Sci., 2000

1999
A Methodological View of Constraint Solving.
Constraints An Int. J., 1999

The Calculus of algebraic Constructions.
Proceedings of the Rewriting Techniques and Applications, 10th International Conference, 1999

The Higher-Order Recursive Path Ordering.
Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

Constraints and Constraint Solving: An Introduction.
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.
Theor. Comput. Sci., 1998

Membership equational logic, calculus of inductive instructions, and rewrite logic.
Proceedings of the 1998 International Workshop on Rewriting Logic and its Applications, 1998

1997
Abstract Data Type Systems.
Theor. Comput. Sci., 1997

1996
A Recursive Path Ordering for Higher-Order Terms in <i>eta</i>-Long <i>beta</i>-Normal Form.
Proceedings of the Rewriting Techniques and Applications, 7th International Conference, 1996

1995
Problems in Rewriting III.
Proceedings of the Rewriting Techniques and Applications, 6th International Conference, 1995

1994
Syntacticness, Cycle-Syntacticness, and Shallow Theories
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).
SIGACT News, 1994

Strong Sequentiality of Left-Linear Overlapping Rewrite Systems.
Proceedings of the Conditional and Typed Rewriting Systems, 4th International Workshop, 1994

Modular Termination of Term Rewriting Systems Revisited.
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.
Proceedings of the Rewriting Techniques and Applications, 5th International Conference, 1993

Introduction to Rewriting.
Proceedings of the Term Rewriting, 1993

1992
Termination and Completion Modulo Associativity, Commutativity and Identity.
Theor. Comput. Sci., 1992

Programming with Equalitiers, Subsorts, Overloading and Parametrization in OBJ.
J. Log. Program., 1992

Decidable Problems in Shallow Equational Theories (Extended Abstract)
Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), 1992

Rewriting Techniques for Software Engineering.
Proceedings of the Recent Trends in Data Type Specification, 1992

1991
Notations for Rewting.
Bull. EATCS, 1991

Executable Higher-Order Algebraic Specifications.
Proceedings of the STACS 91, 1991

Open Problems in Rewriting.
Proceedings of the Rewriting Techniques and Applications, 4th International Conference, 1991

A Computation Model for Executable Higher-Order Algebraic Specification Languages
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.
Proceedings of the Automata, Languages and Programming, 18th International Colloquium, 1991

Solving Equations in Abstract Algebras: A Rule-Based Survey of Unification.
Proceedings of the Computational Logic - Essays in Honor of Alan Robinson, 1991

1990
Syntactic Theories.
Proceedings of the Mathematical Foundations of Computer Science 1990, 1990

Completion modulo Associativity, Commutativity and Identity (AC1).
Proceedings of the Design and Implementation of Symbolic Computation Systems, 1990

Tutorial on Rewrite-Based Theorem Proving.
Proceedings of the 10th International Conference on Automated Deduction, 1990

Rewrite Systems.
Proceedings of the Handbook of Theoretical Computer Science, 1990

1989
Automatic Proofs by Induction in Theories without Constructors
Inf. Comput., July, 1989

Unification in Boolean Rings and Abelian Groups.
J. Symb. Comput., 1989

1988
Unification in Free Extensions of Boolean Rings and Abelian Groups
Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), 1988

OBJ: Programming with Equalities, Subsorts, Overloading and Parameterization.
Proceedings of the Algebraic and Logic Programming, 1988

1987
Reductive conditional term rewriting systems.
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.
SIAM J. Comput., 1986

Automatic Proofs by Induction in Equational Theories Without Constructors
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986

1985
Proofs by induction in equational theories without constructors.
Bull. EATCS, 1985

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

Operational Semantics for Order-Sorted Algebra.
Proceedings of the Automata, 1985

1984
Construction D'un Plus Petit Odre de Simplification.
RAIRO Theor. Informatics Appl., 1984

Termination of a Set of Rules Modulo a Set of Equations.
Proceedings of the 7th International Conference on Automated Deduction, 1984

1983
Church-Rosser Properties of Weakly Terminating Term Rewriting Systems.
Proceedings of the 8th International Joint Conference on Artificial Intelligence. Karlsruhe, 1983

Incremental Construction of Unification Algorithms in Equational Theories.
Proceedings of the Automata, 1983

Confluent and Coherent Equational Term Rewriting Systems: Application to Proofs in Abstract Data Types.
Proceedings of the CAAP'83, 1983

Programming and Checking Data Types with REVE.
Proceedings of the Proceedings 2nd Workshop on Abstract Data Type, 1983

1982
On Multiset Orderings.
Inf. Process. Lett., 1982

Recursive Decomposition Ordering.
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.
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.
Proceedings of the Sixth International Joint Conference on Artificial Intelligence, 1979

1977
SISP/1: An Interactive System Able to Synthesize Functions from Examples.
Proceedings of the 5th International Joint Conference on Artificial Intelligence. Cambridge, 1977


  Loading...