• 
  Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997. IEEE Computer Society 1997 ISBN 0-8186-7925-5

Invited Speaker

Luca Cardelli: A Theory of Objects.

Rewriting & Deduction

• 
  Franz Baader: Combination of Compatible Reduction Orderings that are Total on Ground Terms. 2-13
• 
  Adel Bouhoula, Jean-Pierre Jouannaud: Automata-Driven Automated Induction. 14-25
• 
  Hubert Comon, Florent Jacquemard: Ground Reducibility is EXPTIME-Complete. 26-34
• 
  Roberto Di Cosmo, Delia Kesner: Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Extended Abstract). 35-46

Linear Logic & Game Semantics

• 
  Max I. Kanovich, Takayasu Ito: Temporal Linear Logic Specifications for Concurrent Processes (Extended Abstract). 48-57
• 
  James Laird: Full Abstraction for Functional Languages with Control. 58-67
• 
  Patrick Baillot, Vincent Danos, Thomas Ehrhard, Laurent Regnier: Believe it or not, AJM's Games Model is a Model of Classical Linear Logic. 68-75
• 
  Dominic J. D. Hughes: Games and Definability for System F. 76-86

Model Checking

• 
  Henrik Reif Andersen, Henrik Hulgaard: Boolean Expression Diagrams (Extended Abstract). 88-98
• 
  Stefan Dziembowski, Marcin Jurdzinski, Igor Walukiewicz: How Much Memory is Needed to Win Infinite Games? 99-110
• 
  Michael Huth, Marta Z. Kwiatkowska: Quantitative Analysis and Model Checking. 111-122

Invited Speaker

Anita Feferman: The Saga of Alfred Tarski: From Warszawa to Berkeley.

Tutorial

David A. McAllester: Methods of Automated Complexity for Inference Rules.

Concurrency

• 
  Naoki Kobayashi: A Partially Deadlock-Free Typed Process Calculus. 128-139
• 
  Julian Rathke: Unique Fixpoint Induction for Value-Passing Processes (Extended Abstract). 140-148
• 
  Richard Blute, Josee Desharnais, Abbas Edalat, Prakash Panangaden: Bisimulation for Labelled Markov Processes. 149-158

Temporal Logic & Automata

• 
  Eugene Asarin, Paul Caspi, Oded Maler: A Kleene Theorem for Timed Automata. 160-171
• 
  David Janin: Automata, Tableaus and a Reduction Theorem for Fixpoint Calculi in Arbitrary Complete Lattices. 172-182
• 
  P. S. Thiagarajan, Igor Walukiewicz: An Expressively Complete Linear Time Temporal Logic for Mazurkiewicz Traces. 183-194
• 
  Dexter Kozen: On the Complexity of Reasoning in Kleene Algebra. 195-202

Finite Model Theory

• 
  Leonid Libkin: On the Forms of Locality over Finite Models. 204-215
• 
  Martin Grohe: Large Finite Structures with Few L^k-Types. 216-227
• 
  Kousha Etessami, Moshe Y. Vardi, Thomas Wilke: First-Order Logic with Two Variables and Unary Temporal Logic. 228-235
• 
  Oliver Matz, Wolfgang Thomas: The Monadic Quantifier Alternation Hierarchy over Graphs is Infinite. 236-244

Invited Speaker

Leszek Pacholski: Set Constraints.

Semantics & Domain Theory I

• 
  Peter John Potts, Abbas Edalat, Martín Hötzel Escardó: Semantics of Exact Real Arithmetic. 248-257
• 
  Jon G. Riecke, Anders Sandholm: A Relational Account of Call-by-Value Sequentiality. 258-267
• 
  Marcelo P. Fiore, Gordon D. Plotkin, A. John Power: Complete Cuboidal Sets in Axiomatic Domain Theory. 268-278
• 
  Daniele Turi, Gordon D. Plotkin: Towards a Mathematical Operational Semantics. 280-291

Decidability & Complexity Theory

• 
  Sergei G. Vorobyov: The "Hardest" Natural Decidable Theory. 294-305
• 
  Erich Grädel, Martin Otto, Eric Rosen: Two-Variable Logic with Counting is Decidable. 306-317
• 
  Leszek Pacholski, Wieslaw Szwast, Lidia Tendera: Complexity of Two-Variable Logic with Counting. 318-327
• 
  Guo-Qiang Zhang, William C. Rounds: Complexity of Power Default Reasoning. 328-339

Types and Constraints

• 
  Nevin Heintze, David A. McAllester: On the Cubic Bottleneck in Subtyping and Flow Analysis. 342-351
• 
  Fritz Henglein, Jakob Rehof: The Complexity of Subtype Entailment for Simple Types. 352-361
• 
  Witold Charatonik, Andreas Podelski: Set Constraints with Intersection. 362-372

Tutorial

Hubert Comon: Applications of Tree Automata in Rewriting and Lambda Calculus.

Semantics & Domain Theory II

• 
  Martín Hötzel Escardó, Thomas Streicher: Induction and Recursion on the Partial Real Line via Biquotients of Bifree Algebras. 376-386
• 
  Martin Hofmann, Thomas Streicher: Continuation Models are Universal for Lambda-Mu-Calculus. 387-395
• 
  Mariangiola Dezani-Ciancaglini, Jerzy Tiuryn, Pawel Urzyczyn: Discrimination by Parallel Observers. 396-407

Unification and Higher-Order Logic

• 
  Jean Goubault-Larrecq: Ramified Higher-Order Unification. 410-421
• 
  Iliano Cervesato, Frank Pfenning: Linear Higher-Order Pre-Unification. 422-433
• 
  Raymond McDowell, Dale Miller: A Logic for Reasoning with Higher-Order Abstract Syntax. 434-445