From the reviews: "The book ... gives an overview of Jouannaud's distinguished career and contributions, and provides an impressive list of doctoral descendants. ... will be very useful not only as a reference tool for specialists, but also as an inspiration and source of ideas for budding researchers." (G. Sivakumar, ACM Computing Reviews, Vol. 49 (12), December, 2008)

• Rewriting Foundations.- The Hydra Battle Revisited.- Orderings and Constraints: Theory and Practice of Proving Termination.- Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations.- Computability Closure: Ten Years Later.- Reduction Strategies and Acyclicity.- Proof and Computation.- Towards Rewriting in Coq.- Superdeduction at Work.- Remarks on Semantic Completeness for Proof-Terms with Laird’s Dual Affine/Intuitionistic ?-Calculus.- Linear Recursive Functions.- Towards Safety and Security.- Deducibility Constraints, Equational Theory and Electronic Money.- Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms.- Towards Modular Algebraic Specifications for Pointer Programs: A Case Study.- Modeling Permutations in Coq for Coccinelle.

From the reviews: "The book ... gives an overview of Jouannaud's distinguished career and contributions, and provides an impressive list of doctoral descendants. ... will be very useful not only as a reference tool for specialists, but also as an inspiration and source of ideas for budding researchers." (G. Sivakumar, ACM Computing Reviews, Vol. 49 (12), December, 2008)

• Rewriting Foundations.- The Hydra Battle Revisited.- Orderings and Constraints: Theory and Practice of Proving Termination.- Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations.- Computability Closure: Ten Years Later.- Reduction Strategies and Acyclicity.- Proof and Computation.- Towards Rewriting in Coq.- Superdeduction at Work.- Remarks on Semantic Completeness for Proof-Terms with Laird’s Dual Affine/Intuitionistic ?-Calculus.- Linear Recursive Functions.- Towards Safety and Security.- Deducibility Constraints, Equational Theory and Electronic Money.- Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms.- Towards Modular Algebraic Specifications for Pointer Programs: A Case Study.- Modeling Permutations in Coq for Coccinelle.

From the reviews: "The book ... gives an overview of Jouannaud's distinguished career and contributions, and provides an impressive list of doctoral descendants. ... will be very useful not only as a reference tool for specialists, but also as an inspiration and source of ideas for budding researchers." (G. Sivakumar, ACM Computing Reviews, Vol. 49 (12), December, 2008)

• Rewriting Foundations.- The Hydra Battle Revisited.- Orderings and Constraints: Theory and Practice of Proving Termination.- Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations.- Computability Closure: Ten Years Later.- Reduction Strategies and Acyclicity.- Proof and Computation.- Towards Rewriting in Coq.- Superdeduction at Work.- Remarks on Semantic Completeness for Proof-Terms with Laird’s Dual Affine/Intuitionistic ?-Calculus.- Linear Recursive Functions.- Towards Safety and Security.- Deducibility Constraints, Equational Theory and Electronic Money.- Applying a Theorem Prover to the Verification of Optimistic Replication Algorithms.- Towards Modular Algebraic Specifications for Pointer Programs: A Case Study.- Modeling Permutations in Coq for Coccinelle.