BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Austria
1 × France
1 × Japan
1 × Switzerland
1 × The Netherlands
1 × United Kingdom
2 × Canada
2 × Greece
2 × Poland
2 × Spain
3 × Germany
4 × Italy
7 × USA
Collaborated with:
A.Rubio N.Dershowitz M.Okada H.Kirchner J.Li F.Blanqui J.W.Klop J.Meseguer A.Bouhoula J.Liu P.Strub C.Kirchner J.A.Goguen V.v.Oostrom J.Hsiang E.Kounalis M.Munoz M.Ogawa H.Comon M.Haberstrau A.Boudet M.Schmidt-Schauß B.Barras Q.Wang A.Mégrelis K.Futatsugi
Talks about:
order (11) rewrit (9) equat (7) theori (5) higher (5) problem (4) induct (4) set (4) construct (3) confluenc (3)

Person: Jean-Pierre Jouannaud

DBLP DBLP: Jouannaud:Jean=Pierre

Facilitated 3 volumes:

FPCA 1985Ed
RTA 1985Ed

Contributed to:

CSL 20152015
TLCA 20152015
RTA-TLCA 20142014
CSL 20122012
LICS 20112011
ICALP (2) 20092009
CSL 20082008
CSL 20072007
RTA 20062006
RTA 20052005
LICS 19991999
RTA 19991999
WRLA 19981998
LICS 19971997
RTA 19961996
RTA 19951995
RTA 19931993
LICS 19921992
ICALP 19911991
LICS 19911991
RTA 19911991
CADE 19901990
ALP 19881988
LICS 19881988
LICS 19861986
ICALP 19851985
POPL 19851985
CADE 19841984
POPL 19841984
ICALP 19831983

Wrote 32 papers:

CSL-2015-LiuJO #confluence #term rewriting
Confluence of Layered Rewrite Systems (JL, JPJ, MO), pp. 423–440.
TLCA-2015-JouannaudL #termination
Termination of Dependently Typed Rewrite Rules (JPJ, JL), pp. 257–272.
RTA-TLCA-2014-LiuDJ #analysis #confluence
Confluence by Critical Pair Analysis (JL, ND, JPJ), pp. 287–302.
Church-Rosser Properties of Normal Rewriting (JPJ, JL), pp. 350–365.
LICS-2011-BarrasJSW #decidability #first-order #higher-order #named #type system
CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory (BB, JPJ, PYS, QW), pp. 143–151.
ICALP-v2-2009-JouannaudO #confluence #diagrams
Diagrammatic Confluence and Completion (JPJ, VvO), pp. 212–222.
CSL-2008-BlanquiJR #order
The Computability Path Ordering: The End of a Quest (FB, JPJ, AR), pp. 1–14.
CSL-2007-BlanquiJS #calculus #induction
Building Decision Procedures in the Calculus of Inductive Constructions (FB, JPJ, PYS), pp. 328–342.
RTA-2006-Jouannaud #composition
Modular Church-Rosser Modulo (JPJ), pp. 96–107.
RTA-2006-JouannaudR #higher-order
Higher-Order Orderings for Normal Rewriting (JPJ, AR), pp. 387–399.
RTA-2005-Jouannaud #years after
Twenty Years Later (JPJ), pp. 368–375.
LICS-1999-JouannaudR #higher-order #recursion
The Higher-Order Recursive Path Ordering (JPJ, AR), pp. 402–411.
RTA-1999-BlanquiJO #algebra #calculus
The Calculus of algebraic Constructions (FB, JPJ, MO), pp. 301–316.
WRLA-1998-Jouannaud #calculus #equation #induction #logic
Membership equational logic, calculus of inductive instructions, and rewrite logic (JPJ), pp. 388–393.
LICS-1997-BouhoulaJ #automation #induction
Automata-Driven Automated Induction (AB, JPJ), pp. 14–25.
RTA-1996-JouannaudR #higher-order #normalisation #recursion
A Recursive Path Ordering for Higher-Order Terms in η-Long β-Normal Form (JPJ, AR), pp. 108–122.
RTA-1995-DershowitzJK #problem
Problems in Rewriting III (ND, JPJ, JWK), pp. 457–471.
RTA-1993-DershowitzJK #problem
More Problems in Rewriting (ND, JPJ, JWK), pp. 468–487.
LICS-1992-ComonHJ #decidability #equation #problem
Decidable Problems in Shallow Equational Theories (HC, MH, JPJ), pp. 255–265.
ICALP-1991-JouannaudO #decidability #satisfiability
Satisfiability of Systems of Ordinal Notations with the Subterm Property is Decidable (JPJ, MO), pp. 455–468.
LICS-1991-JouannaudO #algebra #execution #higher-order #specification
A Computation Model for Executable Higher-Order Algebraic Specification Languages (JPJ, MO), pp. 350–361.
RTA-1991-DershowitzJK #problem
Open Problems in Rewriting (ND, JPJ, JWK), pp. 445–456.
CADE-1990-HsiangJ #proving #theorem proving #tutorial
Tutorial on Rewrite-Based Theorem Proving (JH, JPJ), p. 684.
ALP-1988-JouannaudKKM #named #programming
OBJ: Programming with Equalities, Subsorts, Overloading and Parameterization (JPJ, CK, HK, AM), pp. 41–52.
LICS-1988-BoudetJS #unification
Unification in Free Extensions of Boolean Rings and Abelian Groups (AB, JPJ, MSS), pp. 121–130.
LICS-1986-JouannaudK #automation #equation #induction #proving
Automatic Proofs by Induction in Equational Theories Without Constructors (JPJ, EK), pp. 358–366.
ICALP-1985-GoguenJM #algebra #order #semantics
Operational Semantics for Order-Sorted Algebra (JAG, JPJ, JM), pp. 221–231.
Principles of OBJ2 (KF, JAG, JPJ, JM), pp. 52–66.
CADE-1984-JouannaudM #equation #set #termination
Termination of a Set of Rules Modulo a Set of Equations (JPJ, MM), pp. 175–193.
POPL-1984-JouannaudK #equation #set
Completion of a Set of Rules Modulo a Set of Equations (JPJ, HK), pp. 83–92.
ICALP-1983-JouannaudKK #algorithm #equation #incremental #unification
Incremental Construction of Unification Algorithms in Equational Theories (JPJ, CK, HK), pp. 361–373.
TAPSOFT-1997-BouhoulaJM #equation #logic #proving #specification
Specification and Proof in Membership Equational Logic (AB, JPJ, JM), pp. 67–92.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.