2. CTRS 1990: Montreal, Canada

@proceedings{DBLP:conf/ctrs/1990,
  editor    = {St{\'e}phane Kaplan and
               Mitsuhiro Okada},
  title     = {Conditional and Typed Rewriting Systems, 2nd International CTRS
               Workshop, Montreal, Canada, June 11-14, 1990, Proceedings},
  booktitle = {CTRS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {516},
  year      = {1991},
  isbn      = {3-540-54317-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Theory of Condtional and Horn Clause Systems

• François Bronsard, Uday S. Francois: Conditional Rewriting in Focus. 2-13
• Nachum Dershowitz: A Maximal-Literal Unit Strategy for Horn Clauses. 14-25
• Jan Willem Klop, Roel C. de Vrijer: Extended Term Rewriting Systems. 26-50
• Emmanuel Kounalis, Michaël Rusinowitch: A Proof System for Conditional Algebraic Specifications. 51-63
• José Meseguer: Conditional Rewriting Logic: Deduction, Models and Concurrency. 64-91
• Chilukuri K. Mohan: Equivalences of Rewrite Programs. 92-97

Infinite Terms, Non-Terminating Systems, and Termination

• Hong Chen, Jieh Hsiang, Hwa-Chung Kong: On Finite Representations of Infinite Sequences of Terms. 100-114
• Yiyun Chen, Michael J. O'Donnell: Infinite Terms and Infinite Rewritings. 115-126
• Yiyun Chen, Michael J. O'Donnell: Testing Confluence of Nonterminating Rewriting Systems. 127-136
• Bernard R. Hodgson, Clement F. Kent: A Survey of Ordinal Interpretations of Type epsilon₀for Termination of Rewriting Systems. 137-142
• Hélène Kirchner, Miki Hermann: Meta-rule Synthesis from Crossed Rewrite Systems. 143-154

Extension of Knuth-Bendix Completion

• Siva Anantharaman, Maria Paola Bonacina: An Application of Automated Equational Reasoning to Many-valued Logic. 156-161
• Leo Bachmair, Harald Ganzinger: Completion of First-Order Clauses with Equality by Strict Superposition (Extended Abstract). 162-180
• Hubert Bertling: Knuth-Bendix Completion of Horn Clause Programs for Restricted Linear Resolution and Paramodulation. 181-193
• Eddy Bevers, Johan Lewi: Proof by Consistency in Conditional Equational Theories. 194-205
• Maria Paola Bonacina, Jieh Hsiang: Completion Procedures as Semidecision Procedures. 206-232
• Hervé Devie: Linear Completion. 233-245
• Robert Nieuwenhuis, Fernando Orejas: Clausal Rewriting. 246-258

Combined Systems, Combined Languages and Modularity

• Franco Barbanera: Adding Algebraic Rewriting to the Calculus of Constructions: Strong Normalization Preserved. 260-271
• Wadoud Bousdira, Jean-Luc Remy: On Sufficient Completeness of Conditional Specifications. 272-286
• N. Lichtenstein, Stéphane Kaplan: FPL: Functional Plus Logic Programming: An Integration of the FP and Prolog Languages. 287-294
• Aart Middeldorp: Confluence of the Disjoint Union of Conditional Term Rewriting Systems. 295-306
• Detlef Plump: Implementing Term Rewriting by Graph Reduction: Termination of Combined Systems. 307-317

Architecture, Compilers and Parallel Computation

• Hitoshi Aida, Joseph A. Goguen, José Meseguer: Compiling Concurrent Rewriting onto the Rewrite Rule Machine. 320-332
• Sergio Antoy: Design Strategies for Rewrite Rules. 333-341
• Louis Galbiati, Carolyn L. Talcott: A Simplifier for Untyped Lambda Expressions. 342-353
• Marko C. J. D. van Eekelen, Marinus J. Plasmeijer, J. E. W. Smetsers: Parallel Graph Rewriting on Loosely Coupled Machine Architectures. 354-369

Basic Frameworks for Typed and Order-Sorted Systems

• Roberto M. Amadio: Typed Equivalence, Type Assignment, and Type Containment. 372-382
• Martin C. Emele, Rémi Zajac: A Fixed-Point Semantics for Feature Type Systems. 383-388
• John G. Stell: Unique-Sort Order-Sorted Theories: A Description as Monad Morphisms. 389-400
• Yong Sun: Equational Logics (Birkhoff's Method Revisited). 401-406
• Uwe Waldmann: Compatibility of Order-Sorted Rewrite Rules. 407-416

Extension of Unification and Narrowing Techniques

• G. Aguzzi, U. Modigliani, M. Cecilia Verri: An Universal Termination Condition for Solving Goals in Equational Languages. 418-423
• John Darlington, Yike Guo: Constrained Equational Deduction. 424-435
• Tobias Nipkow: Higher-Order Unification, Polymorphism, and Subsorts (Extended Abstract). 436-447
• Zhenyu Qian: Second-Order Unification in the Presence of Linear Shallow Algebraic Equations (Extended Abstract). 448-453
• Wayne Snyder, Christopher Lynch: An Inference System for Horn Clause Logic with Equality: A Foundation for Conditional E-Unification and for Logic Programming in the Presence of Equality. 454-461