My Book
2008
-
Associative commutative rewriting via flattening
Jean-Pierre Jouannaud
draft.
abstract
full draft
-
Uniform Rewriting Proofs in Parameterized Algebras
Jean-Pierre Jouannaud and Benjamin Monate
draft.
-
Higher-Order Orderings for Normal Rewriting
Jean-Pierre Jouannaud and Albert Rubio
Journal submission.
abstract
Full paper
-
Modular Church-Rosser Modulo: the Full Picture
Jean-Pierre Jouannaud and Yoshihito Toyama
abstract
To appear in IJSI
presentation
-
The Computability Path Ordering: the End of a Quest
Frédéric Blanqui, Jean-Pierre Jouannaud and Albert Rubio
Computer Science Logic, Bertoniro, 2008.
abstract
extended abstract
-
From Formal-Proofs to Mathematical proofs: A Safe Incremental Way for building in first Order Decision Procedures
Frédéric Blanqui, Jean-Pierre Jouannaud and Pierre-Yves Strub
Theoretical Computer Science, Track B, Milan, september 2008.
abstract
extended abstract
2007
-
The Blossoming of Finite Semantic Trees
Jean Goubault-Larrecq and Jean-Pierre Jouannaud
Workshop on Programming Logics in memory of Harald Ganzinger,
june 2005.
abstract
Journal submission
-
HORPO with Computability Closure: a Reconstruction
Frédéric Blanqui, Jean-Pierre Jouannaud and Albert Rubio
14th Conference Logic Programming and Automated Reasonning, Yerevan, Armenia, October 2007.
abstract
extended abstract
-
Confluence Properties of Terminating Higher-Order Rewrite Relations.
Jean-Pierre Jouannaud and Femke van Raamsdonk
Mathematical Theories of Abstraction, substitution and naming in Computer Science, ICMS, Edinburgh, mai 2007.
abstract
invited lecture
-
Building Decision Procedures in the Calculus of Inductive Constructions
Frédéric Blanqui, Jean-Pierre Jouannaud and Pierre-Yves Strub
Proc. CSL, Lausanne, september 2007.
abstract
extended abstract
-
Polymorphic Higher-Order Recursive Path Orderings
Jean-Pierre Jouannaud and Albert Rubio
JACM 54(1):1--48.
abstract
full paper
implementation's tarfile, july 30, 2006.
2006
-
Higher-Order Termination: from Kruskal to Computability
Frédéric Blanqui, Jean-Pierre Jouannaud and Albert Rubio
Invited lecture, LPAR'06, LNAI 4246, Springer Verlag.
abstract
extended abstract
Presentation
-
Higher-Order Orderings for Normal Rewriting
Jean-Pierre Jouannaud and Albert Rubio
Proc. RTA'06, LNCS 4098, Springer Verlag.
abstract
extended abstract
-
Modular Church-Rosser Modulo
Jean-Pierre Jouannaud
Proc. RTA'06, LNCS 4098.
abstract
full paper
2005
-
From OBJ to ML to Coq
Jacek Chrzaszcz and Jean-Pierre Jouannaud
Algebra, Meaning and Computation.
Essays dedicated to Joseph A. Goguen on the Occasion of his 65th Birthday, San Diego, June 2006.
LNCS 4060, Springer Verlag.
abstract
full paper
-
Higher-Order Rewriting : Framework, Confluence and Termination
Jean-Pierre Jouannaud
In Processes, Terms and Cycles: Steps on the road to infinity.
Essays dedicated to Jan Willem Klop on the Occasion of his 60th Birthday,
December 2005.
LNCS 3838, Springer Verlag.
abstract
full paper
-
Automatic Complexity Analysis for Programs extracted from Coq Proofs
Jean-Pierre Jouannaud et Weiwen Xu
Workshop CLASE, ETAPS, Edinburgh, april 2005.
abstract
full paper
Presentation
-
Twenty years later
Jean-Pierre Jouannaud
Invited presentation, Rewriting techniques and Applications,
Nara, Japan, april 2005.
abstract
full paper
-
A New Generation of Proof Assistants Integrating Small Proof
Engines
Frédéric Blanqui, Jean-Pierre Jouannaud and Pierre-Yves Strub
Invited presentation, 2nd Taiwanese-French
Conference on Information Technology, Tainan, Taiwan, march 2005.
2004
-
A Calculus of Congruent Constructions
Frédéric Blanqui, Jean-Pierre Jouannaud and Pierre-Yves Strub
draft.
abstract
full draft
-
Formal Mathematics: Application to software safety and Internet Security
Jean-Pierre Jouannaud
Invited presentation, 9th Articifial Intelligence Conference,
Taipei, nov. 2004.
full presentation
-
Theorem Proving languages for verification
Jean-Pierre Jouannaud
Invited presentation, 2nd International Symposium on Automated
Technology for Verification and Analysis, Taipei, nov. 2004.
extended abstract
full presentation
2003
-
Formal Verification of Dynamic Real-Time State-Transition Systems
Using Linear Logic
Koji Hasebe, Jean-Pierre Jouannaud, Antoine Kremer, Mitsuhiro
Okada and Roland Zumkeller
Proc. Software Science Conference, Nagoya, 2003.
abstract
-
FATALIS : Real time processes as linear logic specifications
Vincent Cremet, Koji Hasebe, Jean-Pierre Jouannaud, Antoine Kremer and Mitsuhiro Okada
Proc. Int. Workshop on Automated Verification of Infinite-State
Systems, Varsaw, 2003.
abstract
2002
-
Inductive Data Type Systems
Frédéric Blanqui, Jean-Pierre Jouannaud and Mitsuhiro Okada
Theoretical Computer Science 272(1-2):41-68.
abstract
2001
-
Higher-Order Recursive Path Orderings "à la carte"
Jean-Pierre Jouannaud and Albert Rubio
Invited lecture
In Workshop on Termination, Netherland, april 2001.
full draft
-
Higher-Order Recursive Path Orderings "à la carte"
Jean-Pierre Jouannaud and Albert Rubio
Invited lecture
In First Japonese Conference on Logic and Computation,
Sendai, october 2001.
extended abstract
-
First order constraints in shallow equational theories
Hubert Comon and Jean-Pierre Jouannaud
Proc. International Workshop on Constraints, CIRM, mai 2001.
-
Automata-Driven Automated Induction
Adel Bouhoula and Jean-Pierre Jouannaud
Information and Computation 169:1-22..
abstract
full draft
2000
-
Introducing OBJ
J.A. Goguen, T. Winkler, J. Meseguer, K. Futatsugi and J.P. Jouannaud
In Software Engineering with OBJ : algebraic specification in
action, Goguen and Malcom Editors, Kluwer, 2000.
-
Model checking versus theorem proving for verifying protocols
Jean-Pierre Jouannaud
Invited lecture
In Distributed Systems Verification and Validation, Taipei,
april 2000.
1999
-
Constraints and Constraint Solving: An Introduction
Jean-Pierre Jouannaud and Ralf Treinen
In International CCL Summer School, september 1999.
To appear in LNCS 2002.
abstract
-
Towards Engineering Proofs
Jean-Pierre Jouannaud
Invited lecture
In Logic, Methodology, and Phylosophy of
Science, august 1999, Krakow, Poland.
abstract
-
Specification and Proof in Membership Equational Logic
Adel Bouhoula and Jean-Pierre Jouannaud and Jose Meseguer
Theoretical Computer Science 236:35-132.
abstract
full paper
-
A Methodological View of Constraint Solving
Hubert Comon, Mehmet Dincbas, Jean-Pierre Jouannaud and Claude Kirchner
Constraints 4(4):337-361.
abstract
full paper
-
The Calculus of Algebraic Constructions
Frédéric Blanqui and Jean-Pierre Jouannaud and Mitsuhiro Okada
In Rewriting Techniques and Applications, july 1999, Trento,
Italy.
abstract
extended abstract
full paper
-
The Higher-Order Recursive Path Ordering
Jean-Pierre Jouannaud and Albert Rubio
In IEEE Symposium on Logic in Computer Science, july 1999,
Trento, Italy.
abstract
extended abstract
1998
-
Membership Equational Logic, Calculus of Inductive Constructions, and
Rewrite Logic
Invited lecture
In 2nd Workshop on Rewrite Logic and
Applications, september 1998, Pont à Mousson, France.
Jean-Pierre Jouannaud
abstract
extended abstract
-
Rewrite Orderings for Higher-Order Terms in eta-Long beta-Normal Form
and the Recursive Path Ordering
Jean-Pierre Jouannaud and Albert Rubio
Theoretical Computer Science 208(1-2):33-58.
abstract
full paper
1997
-
Interprétation des langages de programmation
Jean-Pierre Jouannaud, Claude Marché et Ralf Treinen
abstract
draft
- Inductive Data Type Systems: Strong Normalization
Jean-Pierre Jouannaud and Mitsuhiro Okada
abstract
full paper
- Abstract Data Type Systems
Jean-Pierre Jouannaud and Mitsuhiro Okada
Theoretical Computer Science 173(2):349-391.
abstract
full paper
-
Automata-Driven Automated Induction
Adel Bouhoula and Jean-Pierre Jouannaud
In IEEE Symposium on Logic in Computer Science, july 1997, Warsaw,
POLAND.
abstract
extended abstract
-
Specification and Proof in Membership Equational Logic
Adel Bouhoula and Jean-Pierre Jouannaud and Jose Meseguer
in Proc. TAPSOFT'97, Lille, FRANCE, LNCS 1214.
abstract
extended abstract
1996
-
Les Termes en Logique et en Programmation
Hubert Comon et Jean-Pierre Jouannaud
abstract
draft
-
A Recursive Path Ordering for Higher-Order Terms in eta-Long beta-Normal Form
Jean-Pierre Jouannaud and Albert Rubio
in Proc. RTA'96, New-Brunswick, New-Jersey, USA, LNCS 1103.
abstract
extended abstract
1995
- Rewrite Proofs and Computations
Jean-Pierre Jouannaud
in Proof and Computation, Helmut Schwichtenberg editor,
NATO series F: Computer and Systems Sciences, vol 139, pp 173-218, Springer Verlag.
abstract
full paper
1994
- Strong Sequentiality of Left-Linear Overlapping Rewrite
Systems
Jean-Pierre Jouannaud and Walid Sadfi
in Proc. CTRS'94, Jerusalem, LNCS 968.
abstract
full paper
- Modular Termination of Term Rewriting Systems Revisited
Maribel Fernandez and Jean-Pierre Jouannaud
in Recent Trends in Data Type Specification,
Egidio Astesiano, Gianna Reggio and Andrzej Tarlecki editors,
LNCS 906.
abstract
full paper
- Syntacticness, Cycle-Syntacticness and Shallow Theories
Hubert Comon, Marianne Haberstrau and Jean-Pierre Jouannaud
Information and Computation 111(1):154-191
abstract
full paper
Last change: July 23, 1996.
In case of problems: please contact
Ralf Treinen.