21. LICS 2006: Seattle, WA, USA

Introduction

• Foreward.
  
• Conference Organization.
  
• Organizing Committee.
  
• Reviewers.
  

Plenary Talk

• Randal E. Bryant:
  Formal Verification of Infinite State Systems Using Boolean Methods. 3-4
  

Session 1: Complexity and Decidability

• Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin, Claire David:
  Two-Variable Logic on Words with Data. 7-16
  
• Stéphane Demri, Ranko Lazic:
  LTL with the Freeze Quantifier and Register Automata. 17-26
  
• Guoqiang Pan, Moshe Y. Vardi:
  Fixed-Parameter Hierarchies inside PSPACE. 27-36
  
• Martin Otto:
  The Boundedness Problem for Monadic Universal First-Order Logic. 37-48
  

Session 2: Concurrency

• Marcelo P. Fiore, Sam Staton:
  A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics. 49-58
  
• Catuscia Palamidessi, Vijay A. Saraswat, Frank D. Valencia, Björn Victor:
  On the Expressiveness of Linearity vs Persistence in the Asychronous Pi-Calculus. 59-68
  
• Filippo Bonchi, Barbara König, Ugo Montanari:
  Saturated Semantics for Reactive Systems. 69-80
  

Session 3: Pushdown Systems

• C.-H. Luke Ong:
  On Model-Checking Trees Generated by Higher-Order Recursion Schemes. 81-90
  
• Dietrich Kuske, Markus Lohrey:
  Monadic Chain Logic Over Iterations and Applications to Pushdown Systems. 91-100
  
• Vineet Kahlon, Aarti Gupta:
  An Automata-Theoretic Approach for Model Checking Threads for LTL Propert. 101-110
  
• Tachio Terauchi, Alex Aiken:
  On Typability for Rank-2 Intersection Types with Polymorphic Recursion. 111-122
  

Invited Talk

• Andreas Blass:
  Adapting Logics. 123
  

Session 4: Logics of Program

• Adam Barth, John C. Mitchell:
  Managing Digital Rights using Linear Logic. 127-136
  
• Matthew J. Parkinson, Richard Bornat, Cristiano Calcagno:
  Variables as Resource in Hoare Logics. 137-146
  
• Jonathan Hayman, Glynn Winskel:
  Independence and Concurrent Separation Logic. 147-156
  
• Daniel Leivant:
  Matching Explicit and Modal Reasoning about Programs: A Proof Theoretic Delineation of Dynamic Logic. 157-168
  

Session 5: Proof Theory

• Ugo Dal Lago:
  Context Semantics, Linear Logic and Computational Complexity. 169-178
  
• Olivier Laurent, Lorenzo Tortora de Falco:
  Obsessional Cliques: A Semantic Characterization of Bounded Time Complexity. 179-188
  
• Alexis Maciel, Toniann Pitassi:
  Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives. 189-200
  

Session 6: Model Theory

• Benoit Larose, Cynthia Loten, Claude Tardif:
  A Characterisation of First-Order Constraint Satisfaction Problems. 201-210
  
• Laura Chaubard, Jean-Eric Pin, Howard Straubing:
  First Order Formulas with Modular Ppredicates. 211-220
  
• Emil W. Kiss, Matthew Valeriote:
  On Tractability and Congruence Distributivity. 221-230
  
• Lutz Schröder, Dirk Pattinson:
  PSPACE Bounds for Rank-1 Modal Logics. 231-242
  

Invited Talk

• Orna Kupferman:
  Avoiding Determinization. 243-254
  

Session 7: Temporal Logics and Automata

• Nir Piterman:
  From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata. 255-264
  
• Orna Kupferman, Moshe Y. Vardi:
  Memoryful Branching-Time Logic. 265-274
  
• Nir Piterman, Amir Pnueli:
  Faster Solutions of Rabin and Streett Games. 275-284
  
• Mikolaj Bojanczyk, Thomas Colcombet:
  Bounds in w-Regularity. 285-296
  

Session 8: Lambda Calculus

• Søren B. Lassen:
  Head Normal Form Bisimulation for Pairs and the \lambda\mu-Calculus. 297-306
  
• Thierry Coquand, Arnaud Spiwack:
  A Proof of Strong Normalisation using Domain Theory. 307-316
  
• Giulio Manzonetto, Antonino Salibra:
  Boolean Algebras for Lambda Calculus. 317-326
  
• Makoto Tatsuta, Mariangiola Dezani-Ciancaglini:
  Normalisation is Insensible to lambda-Term Identity or Difference. 327-338
  

Keynote Session: Celebrating Birth Centennial of Kurt Godel

• John W. Dawson:
  Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science. 339-341
  

Invited Talk

• Andrew D. Gordon:
  Provable Implementations of Security Protocols. 345-346
  

Session 9: Timed and Stochastic Systems

• Tomás Brázdil, Václav Brozek, Vojtech Forejt, Antonín Kucera:
  Stochastic Games with Branching-Time Winning Objectives. 349-358
  
• Dexter Kozen:
  Coinductive Proof Principles for Stochastic Processes. 359-366
  
• Patricia Bouyer, Thomas Brihaye, Fabrice Chevalier:
  Control in o-minimal Hybrid Systems. 367-378
  

Session 10: Verification

• Thomas Ball, Orna Kupferman:
  An Abstraction-Refinement Framework for Multi-Agent Systems. 379-388
  
• Daniele Varacca, Hagen Völzer:
  Temporal Logics and Model Checking for Fairly Correct Systems. 389-398
  
• Sharon Shoham, Orna Grumberg:
  3-Valued Abstraction: More Precision at Less Cost. 399-410
  

Session 11: Approximations

• Anuj Dawar, Martin Grohe, Stephan Kreutzer, Nicole Schweikardt:
  Approximation Schemes for First-Order Definable Optimisation Problems. 411-420
  
• Eldar Fischer, Frédéric Magniez, Michel de Rougemont:
  Approximate Satisfiability and Equivalence. 421-430