16. LICS 2001: Boston, Massachusetts, USA

Invited Talk

• John C. Mitchell, Ajith Ramanathan, Andre Scedrov, Vanessa Teague: Probabilistic Polynominal-Time Process Calculus and Security Protocol Analysis. 3-8

Session 1

• Frédéric Blanqui: Definitions by Rewriting in the Calculus of Constructions. 9-18
• Harald Rueß, Natarajan Shankar: Deconstructing Shostak. 19-28
• Aaron Stump, Clark W. Barrett, David L. Dill, Jeremy R. Levitt: A Decision Procedure for an Extensional Theory of Arrays. 29-37
• Guillem Godoy, Robert Nieuwenhuis: On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups. 38-50

Invited Talk

• Satyaki Das, David L. Dill: Successive Approximation of Abstract Transition Relations. 51-60

Session 2

• Scott D. Stoller: A Bound on Attacks on Payment Protocols. 61-70
• Lefteris M. Kirousis, Phokion G. Kolaitis: A Dichotomy in the Complexity of Propositional Circumscription. 71-80
• Harald Ganzinger: Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems. 81-92

Session 3

• Marcelo P. Fiore, Daniele Turi: Semantics of Name and Value Passing. 93-104
• James Laird: A Fully Abstract Game Semantics of Local Exceptions. 105-114
• Martín Hötzel Escardó, Alex K. Simpson: A Universal Characterization of the Closed Euclidean Interval. 115-128

Invited Talk

• Yuri Gurevich: Logician in the Land of OS: Abstract State Machines in Microsoft. 129-138

Session 4

• Jeremy Avigad: Eliminating Definitions and Skolem Functions in First-Order Logic. 139-146
• Wieslaw Szwast, Lidia Tendera: On the Decision Problem for the Guarded Fragment with Transitivity. 147-156
• André Arnold, Giacomo Lenzi, Jerzy Marcinkowski: The Hierarchy inside Closed Monadic Sigma₁ Collapses on the Infinite Binary Tree. 157-166
• Taneli Huuskonen, Tapani Hyttinen: On Definability of Order in Logic with Choice. 167-176

Invited Talk

• Wolfgang Thomas: The Engineering Challenge for Logic.

Session 5

• Stephen A. Cook, Antonina Kolokolova: A Second-Order System for Polytime Reasoning Using Graedel's Theorem. 177-186
• David A. Mix Barrington, Neil Immerman, Clemens Lautemann, Nicole Schweikardt, Denis Thérien: The Crane Beach Conjecture. 187-196
• Micah Adler, Neil Immerman: An n! Lower Bound on Formula Size. 197-

Session 6

• Kazushige Terui: Light Affine Calculus and Polytime Strong Normalization.
• Frank Pfenning: Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory.
• Hongwei Xi: Dependent Types for Program Termination Verification.

Short Paper Session

Invited Talk

• Andrew W. Appel: Foundational Proof-Carrying Code.

Session 7

• Dexter Kozen, Jerzy Tiuryn: Intuitionistic Linear Logic and Partial Correctness. 259-268
• Eugene Asarin, Ahmed Bouajjani: Perturbed Turing Machines and Hybrid Systems. 269-278
• Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar: From Verification to Control: Dynamic Programs for Omega-Regular Objectives. 279-290
• Rajeev Alur, Salvatore La Torre: Deterministic Generators and Games for LTL Fragments. 291-302

Session 8

• Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott: Normalization by Evaluation for Typed Lambda Calculus with Coproducts. 303-310
• Nobuko Yoshida, Martin Berger, Kohei Honda: Strong Normalisation in the pi-Calculus. 311-322
• Alan Jeffrey: A Symbolic Labelled Transition System for Coinductive Subtyping of F_µ< Types. 323-333
• Antonino Salibra: A Continuum of Theories of Lambda Calculus without Semantics. 334-346

Session 9

• David Janin, Giacomo Lenzi: Relating Levels of the Mu-Calculus Hierarchy and Levels of the Monadic Hierarchy. 347-356
• Martin Lange, Colin Stirling: Focus Games for Satisfiability and Completeness of Temporal Logic. 357-365
• Panagiotis Manolios, Richard J. Trefler: Safety and Liveness in Branching Time. 366-

Short Papers

• Serge Abiteboul: Semistructured Data: from Practice to Theory. 379-

Session 10

• Orna Kupferman, Moshe Y. Vardi: Synthesizing Distributed Systems.
• Ahmed Bouajjani, Anca Muscholl, Tayssir Touili: Permutation Rewriting and Algorithmic Verification.
• Glenn Bruns, Patrice Godefroid: Temporal Logic Query Checking. 409-417

Session 11

• Noga Alon, Tova Milo, Frank Neven, Dan Suciu, Victor Vianu: Typechecking XML Views of Relational Databases. 421-430
• Michael Benedikt, Leonid Libkin, Thomas Schwentick, Luc Segoufin: A Model-Theoretic Approach to Regular String Relations. 431-