My Book

2008

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 Internaôiona, S{mposium 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.