16. LICS 2001: Boston, Massachusetts, USA

16th Annual IEEE Symposium on Logic in Computer Science, 16-19 June 2001, Boston, Massachusetts, USA, Proceedings. IEEE Computer Society, 2001, ISBN 0-7695-1281-X

Invited Talk

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

Session 1

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

Invited Talk

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

Session 2

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

Session 3

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

Invited Talk

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

Session 4

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

Invited Talk

Wolfgang Thomas: The Engineering Challenge for Logic. BibTeX

Session 5

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

Session 6

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

Short Paper Session

Invited Talk

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

Session 7

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

Session 8

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

Session 9

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

Short Papers

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

Session 10

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

Session 11

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