The Computability Path Ordering: the End of a Quest (2009)
Frédéric Blanqui, Jean-pierre Jouannaud, Albert Rubio
Abstract. In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an...
Modular Church-Rosser Modulo: The Full Picture (2009)
Jean-pierre Jouannaud, Yoshihito Toyama
Abstract. In [17], Toyama proved that the union of two confluent term-rewriting systems that share absolutely no function symbols or constants is likewise confluent, a property called modularity. The...
The Blossom of Finite Semantic Trees Jean Goubault-Larrecq1 ⋆ 2 ⋆ ⋆ ⋆ ⋆ ⋆ (2008)
This paper is dedicated to the memory of Harald Ganzinger.
Higher-order termination: From kruskal to computability (2008)
Frédéric Blanqui, Jean-pierre Jouannaud, Albert Rubio
Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In...
The computability path ordering: the end of a quest (2008)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Rubio, Albert
In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved...
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Strub, Pierre-Yves
We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, which truly extends...
Jacek Chrz ˛aszcz, Jean-pierre Jouannaud
This work is dedicated to our colleague Joseph Goguen, who was extremely influential in the design of modern programming languages. 1
Associative-commutative rewriting via flattening (2008)
Abstract. AC-rewriting is simulated by using flattened terms, flattened rewrite rules, extensions and specializations with respect to the AC-operators, therefore allowing us to reduce AC-pattern...
HORPO with Computability Closure: A Reconstruction (2008)
Frédéric Blanqui, Jean-pierre Jouannaud, Albert Rubio
Abstract. This paper provides a new, decidable definition of the higherorder recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the...
Abstract. The first RTA conference took place in Dijon, in 1985. This year, 2005, it takes place in Nara. Nara and Dijon share a glorious past but can be considered as being “Sleeping Beauties”,...
Chapter 6 of Handbook of Theoretical Computer Science Volume B: Formal Methods and Semantics (2008)
Nachum Dershowitz, Jean-pierre Jouannaud
J. van Leeuwen, ed.
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Strub, Pierre-Yves
We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, which truly extends...
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Strub, Pierre-Yves
We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, which truly extends...
The computability path ordering: the end of a quest (2008)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Rubio, Albert
In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved...
The computability path ordering: the end of a quest (2008)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Rubio, Albert
In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved...
Fréderic Blanqui, Jean-pierre Jouannaud, Pierre-yves Strub
(CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, which truly extends CIC by building in arbitrary first-order decision procedures: deduction is...
Jean-pierre Jouannaud, Albert Rubio
: This paper extends the termination proof techniques based on rewrite orderings to a higher-order setting, by defining a recursive path ordering for simply typed higher-order terms in j-long...
Higher-Order Recursive Path Orderings à la carte (2007)
Jean-pierre Jouannaud, Albert Rubio
Introduction Rewrite rules are increasingly used in programming languages and logical systems, with two main goals: defining functions by pattern matching; describing rule-based decision procedures....
HORPO with Computability Closure : A Reconstruction (2007)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Rubio, Albert
This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability...
Building Decision Procedures in the Calculus of Inductive Constructions (2007)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Strub, Pierre-Yves
It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when replacing the proof...
Building Decision Procedures in the Calculus of Inductive Constructions (2007)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Strub, Pierre-Yves
It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when replacing the proof...
Building Decision Procedures in the Calculus of Inductive Constructions (2007)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Strub, Pierre-Yves
It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when replacing the proof...
Building Decision Procedures in the Calculus of Inductive Constructions (2007)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Strub, Pierre-Yves
It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when replacing the proof...
Building Decision Procedures in the Calculus of Inductive Constructions (2007)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Strub, Pierre-Yves
It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when replacing the proof...
HORPO with Computability Closure : A Reconstruction (2007)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Rubio, Albert
This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability...
HORPO with Computability Closure : A Reconstruction (2007)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Rubio, Albert
This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability...
Building decision procedures in the calculus of inductive constructions (2007)
Frédéric Blanqui, Jean-pierre Jouannaud, Pierre-yves Strub
It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when replacing the proof...
The Calculus of Algebraic Constructions (2006)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Okada, Mitsuhiro
This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalizes inductive types...
The Calculus of Algebraic Constructions (2006)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Okada, Mitsuhiro
This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalizes inductive types...
The Calculus of Algebraic Constructions (2006)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Okada, Mitsuhiro
This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalizes inductive types...
Inductive-data-type Systems (2006)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Okada, Mitsuhiro
In a previous work (``Abstract Data Type Systems'', TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed...
Higher-Order Termination: from Kruskal to Computability (2006)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Rubio, Albert
Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In...
Higher-Order Termination: from Kruskal to Computability (2006)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Rubio, Albert
Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In...
Higher-Order Termination: from Kruskal to Computability (2006)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Rubio, Albert
In this paper, we reformulate and improve a recent idea of Blanqui (see the paper "(HO)RPO Revisited") by defining a new version of the HORPO with computability closure which integrates smoothly the...
Higher-Order Termination: from Kruskal to Computability (2006)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Rubio, Albert
In this paper, we reformulate and improve a recent idea of Blanqui (see the paper "(HO)RPO Revisited") by defining a new version of the HORPO with computability closure which integrates smoothly the...
Higher-Order Termination: from Kruskal to Computability (2006)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Rubio, Albert
Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In...
Higher-Order Termination: from Kruskal to Computability (2006)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Rubio, Albert
Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In...
cover. Lecture Notes in Computer Science, 3989:178–193, 2006. (2006)
I. Aktug, Computer Science, Pages Springer, Mattias Johansson, Gunnar Kreitz, ...
[7] J. Håstad. The security of the IAPM and IACBC modes. Journal of
Higher-order orderings for normal rewriting (2006)
Jean-pierre Jouannaud, Albert Rubio
Abstract. We extend the termination proof methods based on reduction orderings to higher-order rewriting systems à la Nipkow using higher-order pattern matching for firing rules, and accommodate for...
Higher-order termination: from Kruskal to computability (2006)
Frédéric Blanqui, Jean-pierre Jouannaud, Albert Rubio
Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In...
Polymorphic higher-order recursive path orderings (2005)
Jean-pierre Jouannaud, Lix École Polytechnique, Albert Rubio
This paper extends the termination proof techniques based on reduction orderings to a higherorder setting, by defining a family of recursive path orderings for terms of a typed lambda-calculus...
Higher-Order rewriting: Framework, Confluence and termination (2005)
Equations are ubiquitous in mathematics and in computer science as well. This first sentence of a survey on first-order rewriting borrowed again and again characterizes best the fundamental reason...
Inductive-data-type Systems (2002)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Okada, Mitsuhiro
In a previous work (``Abstract Data Type Systems'', TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed...
Inductive-data-type Systems (2002)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Okada, Mitsuhiro
In a previous work (``Abstract Data Type Systems'', TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed...
Inductive-data-type Systems (2002)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Okada, Mitsuhiro
In a previous work (``Abstract Data Type Systems'', TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed...
The Calculus of Algebraic Constructions (1999)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Okada, Mitsuhiro
This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalizes inductive types...
The Calculus of Algebraic Constructions (1999)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Okada, Mitsuhiro
This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalizes inductive types...
The Calculus of Algebraic Constructions (1999)
Blanqui, Frédéric, Jouannaud, Jean-Pierre, Okada, Mitsuhiro
This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalizes inductive types...
Higher-Order Recursive Path Orderings (1999)
Jean-pierre Jouannaud, Albert Rubio
: This paper extends the termination proof techniques based on reduction orderings to a higher-order setting, by adapting the recursive path ordering definition to higher-order simplytyped -terms....
Inductive Data Type Systems (1999)
Frédéric Blanqui, Jean-pierre Jouannaud, Mitsuhiro Okada
: In a previous work ("Abstract Data Type Systems", TCS 173(2):349--391 (1997)), the last two authors presented a combined language made of a (strongly normalizable) algebraic rewriting...
The Calculus of Algebraic Constructions (1999)
Frederic Blanqui, Jean-Pierre Jouannaud, Mitsuhiro Okada
This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalizes inductive types...
Higher-Order Recursive Path Orderings (1999)
Jean-pierre Jouannaud, Albert Rubio
: This paper extends the termination proof techniques based on reduction orderings to a higher-order setting, by adapting the recursive path ordering definition to higher-order simplytyped -terms....
The Calculus of Algebraic Constructions (1999)
Jean-pierre Jouannaud, Mitsuhiro Okada
This paper is concerned with the foundations of the Calculus of Algebraic Constructions (CAC), an extension of the Calculus of Constructions by inductive data types. CAC generalizes inductive types...
Jean-Pierre Jouannaud LRI, CNRS and Universit'e de Paris-Sud Bat 490, 91405 Orsay Cedex, France Email: Jean-Pierre.Jouannaud@lri.fr 1 Supported by the ESPRIT Research Contract CCL. This paper is...
Inductive Data Type Systems (1998)
Frédéric Blanqui, Jean-pierre Jouannaud, Mitsuhiro Okada
: In a previous work ("Abstract Data Type Systems", TCS 173(2):349--391 (1997)), the last two authors presented a combined language made of a (strongly normalizable) algebraic rewriting...
Abstract Data Type Systems (1997)
Jean-pierre Jouannaud, Mitsuhiro Okada
In a previous work ("Abstract Data Type Systems", TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and...
Inductive Data Type Systems: Strong Normalization (1997)
Jean-pierre Jouannaud, Mitsuhiro Okada
: This paper is concerned with the foundations of Inductive Data Type Systems, an extension of pure type systems by inductive data types. IDTS generalize (inductive) types equipped with primitive...
Inductive Data Type Systems: Strong Normalization (1997)
Jean-pierre Jouannaud, Mitsuhiro Okada
: This paper is concerned with the foundations of Inductive Data Type Systems, an extension of pure type systems by inductive data types. IDTS generalize (inductive) types equipped with primitive...
Abstract Data Type Systems (1997)
Frédéric Blanqui, Jean-pierre Jouannaud, Mitsuhiro Okada
In a previous work (“Abstract Data Type Systems”, TCS 173(2), 1997), the last two authors presented a combined language made of a (strongly normalizing) algebraic rewrite system and a typed...
A Recursive Path Ordering for Higher-Order Terms in η-Long β-Normal Form (1996)
Jean-pierre Jouannaud, Albert Rubio
: This paper extends the termination proof techniques based on rewrite orderings to a higher-order setting, by defining a recursive path ordering for simply typed higher-order terms in j-long...
A Methodological View of Constraint Solving (1996)
Hubert Comon, Mehmet Dincbas, Jean-pierre Jouannaud, Claude Kirchner
Constraints have become very popular during the last decade. Constraints allow to define sets of data by means of logical formulae. Our goal here is to survey the notion of constraint system and to...
A Recursive Path Ordering for Higher-Order Terms in η-Long β-Normal Form (1996)
Jean-pierre Jouannaud, Albert Rubio
: This paper extends the termination proof techniques based on rewrite orderings to a higher-order setting, by defining a recursive path ordering for simply typed higher-order terms in j-long...
Automata-Driven Automated Induction (1996)
Adel Bouhoula, Jean-pierre Jouannaud
. This work investigates inductive theorem proving techniques for first-order functions whose meaning and domains can be specified by Horn Clauses built up from the equality and finitely many unary...
Specification and Proof in Membership Equational Logic (1996)
Adel Bouhoula, Jean-pierre Jouannaud, Jos'e Meseguer
: This paper is part of a long-term effort to increase expressiveness of algebraic specification languages while at the same time having a simple semantic basis on which efficient execution by...
Automata-Driven Automated Induction (1996)
Adel Bouhoula, Jean-pierre Jouannaud
This work investigates inductive theorem proving techniques for first-order functions whose meaning and domains can be specified by Horn Clauses built up from the equality and finitely many unary...
Specification and Proof in Membership Equational Logic (1996)
Adel Bouhoula, Jean-pierre Jouannaud, José Meseguer
This paper is part of a long term effort to increase expressiveness of algebraic specification languages while at the same time having a simple semantic basis on which efficient execution by...
Programming Languages and Dimensions (1996)
Andrew John Kennedy, Francis Davey, Jean Goubault, Barney Hilken, Jean-pierre Jouannaud, Mikael Rittri, ...
Scientists and engineers must ensure that the equations and formulae which they use are dimensionally consistent, but existing programming languages treat all numeric values as dimensionless. This...
Problems in rewriting III (1995)
Nachum Dershowitz, Jean-pierre Jouannaud, Jan Willem Klop
We presented lists of open problems in the theory of rewriting in the proceedings of the previous two conferences [36; 37]. We continue with that tradition this year. We give references to solutions...
Rewrite Proofs and Computations (1995)
. Rewriting is a general paradigm for expressing computations in various logics, and we focus here on rewriting techniques in equational logic. When used at the proof level, rewriting provides with a...
Modular Termination of Term Rewriting Systems Revisited (1995)
Maribel Fernández, Jean-pierre Jouannaud
This paper is concerned with the impact of stepwise development methodologies on prototyping.
Problems in Rewriting III (1995)
Nachum Dershowitz, Jean-pierre Jouannaud, Jan Willem Klop
Introduction We presented lists of open problems in the theory of rewriting in the proceedings of the previous two conferences [ 36; 37 ] . We continue with that tradition this year. We give...
Syntacticness, Cycle-Syntacticness and Shallow Theories (1994)
Hubert Comon, Marianne Haberstrau, Jean-pierre Jouannaud
Solving equations in the free algebra T (F; X) (i.e. unification) uses the two rules: f(~s) = f( ~ t) ! ~s = ~ t (decomposition) and s[x] = x !? (occur-check). These two rules are not correct in...
Syntacticness, Cycle-Syntacticness and Shallow Theories (1994)
Hubert Comon Marianne, Marianne Haberstrau, Jean-pierre Jouannaud
Solving equations in the free algebra T (F; X) (i.e. unification) uses the two rules: f(~s) = f( ~ t) ! ~s = ~ t (decomposition) and s[x] = x !? (occur-check). These two rules are not correct in...
Strong Sequentiality of Left-Linear Overlapping Rewrite Systems (1994)
Jean-pierre Jouannaud, Walid Sadfi
. Confluent term rewriting systems can be seen as a model for functional computations, in which redexes corresponding to instances of left hand sides of rules are repeatedly replaced by their...
More problems in rewriting (1993)
Nachum Dershowitz, Jean-pierre Jouannaud, Jan Willem Klop
Two years ago, in the proceedings of the previous conference, we presented a list of open problems in the theory of rewriting [Dershowitz et al., 1991a]. This time, we report on progress made during...
Joseph A. Goguen, Timothy Winkler, José Meseguer, Kokichi Futatsugi, Jean-Pierre Jouannaud
This is an introduction to OBJ, describing its philosophy, its syntax, its history, and aspects of its semantics, both logical and operational. Many examples are given, using Release 2 of OBJ3, which...
More Problems in Rewriting (1993)
Nachum Dershowitz, Jean-Pierre Jouannaud, Jan Willem Klop
Introduction Two years ago, in the proceedings of the previous conference, we presented a list of open problems in the theory of rewriting [ Dershowitz et al., 1991a ] . This time, we report on...
Termination and Completion modulo Associativity, Commutativity and Identity (1992)
Jean-pierre Jouannaud, Claude Marché
Rewriting with associativity, commutativity and identity has been an open problem for a long time. In 1989, Baird, Peterson and Wilkerson introduced the notion of constrained rewriting, to avoid the...
Open Problems in Rewriting (1991)
Nachum Dershowitz, Jean-pierre Jouannaud, Jan Willem Klop
Introduction Interest in the theory and applications of rewriting has been growing rapidly, as evidenced in part by four conference proceedings (including this one) [15, 26, 41, 66]; three workshop...
Nachum Dershowitz, Jean-Pierre Jouannaud
Completion Completion has recently been put in a more abstract framework [ Bachmair-et al, 1986 ] , an approach we adopt here. As in traditional proof theory (cf. [ Takeuti, 1987 ] ), proofs are...
Church-Rosser properties of weakly terminating term rewriting systems (1983)
Jean-pierre Jouannaud, Helene Kirchner, Jean-luc Remy, F Vandoeuvre, Nancy Cedex
The well known Knuth and Bendix completion procedure computes a convergent term rewriting system from a given set of equational axioms. This procedure was extended to handle mixed sets of rules and...
Fr´ederic Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
We investigate here a new version of the Calculus of Inductive Constructions (CIC) on which the proof assistant Coq is based: the Calculus of Congruent Inductive Constructions, which truly extends...