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-5
  

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-47
  

Invited Talk

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

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-90
  

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-125
  

Invited Talk

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

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-172
  

Invited Talk

• Wolfgang Thomas: The Engineering Challenge for Logic. 173-176

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-206
  

Session 6

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

Short Paper Session

Invited Talk

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

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-300
  

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-343
  

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-374
  

Short Papers

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

Session 10

• Orna Kupferman, Moshe Y. Vardi:
  Synthesizing Distributed Systems. 389-398
  
• Ahmed Bouajjani, Anca Muscholl, Tayssir Touili:
  Permutation Rewriting and Algorithmic Verification. 399-408
  
• 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-440
  

Last update Wed May 22 16:08:33 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page