22. LICS 2007: Wroclaw, Poland

Type Theory

• Andreas Abel, Thierry Coquand, Peter Dybjer:
  Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements. 3-12
  
• Colin Riba:
  Strong Normalization as Safe Interaction. 13-22
  
• Wojciech Moczydlowski:
  A Dependent Set Theory. 23-34
  

Computational Proof Theory

• Thomas C. Hales:
  Some Methods of Problem Solving in Elementary Geometry. 35-40
  
• Paul Brauner, Clément Houtmann, Claude Kirchner:
  Principles of Superdeduction. 41-50
  
• James Brotherston, Alex Simpson:
  Complete Sequent Calculi for Induction and Infinite Descent. 51-62
  

Security

• Michael O. Rabin, Rocco A. Servedio, Christopher Thorpe:
  Highly Efficient Secrecy-Preserving Proofs of Correctness of Computations and Applications. 63-76
  
• Mika Cohen, Mads Dam:
  A Complete Axiomatization of Knowledge and Cryptography. 77-88
  

Timed and Stochastic Systems

• Hugo Gimbert, Wieslaw Zielonka:
  Limits of Multi-Discounted Markov Decision Processes. 89-98
  
• Luca de Alfaro, Rupak Majumdar, Vishwanath Raman, Mariëlle Stoelinga:
  Game Relations and Metrics. 99-108
  
• Patricia Bouyer, Nicolas Markey, Joël Ouaknine, James Worrell:
  The Cost of Punctuality. 109-120
  

Verification

• Mikolaj Bojanczyk:
  Two-way unary temporal logic over trees. 121-130
  
• Marcin Jurdzinski, Ranko Lazic:
  Alternation-free modal mu-calculus for data trees. 131-140
  
• Angelo Montanari, Gabriele Puppis:
  A Contraction Method to Decide MSO Theories of Deterministic Trees. 141-150
  
• Rajeev Alur, Marcelo Arenas, Pablo Barceló, Kousha Etessami, Neil Immerman, Leonid Libkin:
  First-Order and Temporal Logics for Nested Words. 151-160
  
• Salvatore La Torre, Parthasarathy Madhusudan, Gennaro Parlato:
  A Robust Class of Context-Sensitive Languages. 161-170
  
• Francesco Ranzato, Francesco Tapparo:
  A New Efficient Simulation Equivalence Algorithm. 171-180
  
• Detlef Kähler, Ralf Küsters, Tomasz Truderung:
  Infinite State AMC-Model Checking for Cryptographic Protocols. 181-192
  

Constraints

• László Egri, Benoit Larose, Pascal Tesson:
  Symmetric Datalog and Constraint Satisfaction Problems in Logspace. 193-202
  
• Manuel Bodirsky, Hubie Chen:
  Quantified Equality Constraints. 203-212
  
• Pawel M. Idziak, Petar Markovic, Ralph McKenzie, Matthew Valeriote, Ross Willard:
  Tractability and learnability arising from algebras with few subpowers. 213-224
  

Proof Complexity

• Steven James Perron:
  Examining The Fragments of G. 225-234
  
• Phuong Nguyen:
  Separating DAG-Like and Tree-Like Proof Systems. 235-244
  
• Phuong Nguyen, Stephen A. Cook:
  The Complexity of Proving the Discrete Jordan Curve Theorem. 245-256
  

Finite Model Theory

• Phokion G. Kolaitis:
  Reflections on Finite Model Theory. 257-269
  
• Anuj Dawar, Martin Grohe, Stephan Kreutzer:
  Locally Excluding a Minor. 270-279
  
• Balder ten Cate, Johan van Benthem, Jouko A. Väänänen:
  Lindstrom theorems for fragments of first-order logic. 280-292
  

Concurrency and Process Calculi

• Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii:
  Environmental Bisimulations for Higher-Order Languages. 293-302
  
• Marcello M. Bonsangue, Alexander Kurz:
  Pi-Calculus in Logical Form. 303-312
  
• Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, Carroll Morgan, Chenyi Zhang:
  Characterising Testing Preorders for Finite Probabilistic Processes. 313-325
  

Semantics of Programming Languages

• Colin Stirling:
  Higher-Order Matching, Games and Automata. 326-335
  
• Bartek Klin:
  Bialgebraic Operational Semantics and Modal Logic. 336-345
  
• Rasmus Ejlers Møgelberg, Alex Simpson:
  Relational Parametricity for Computational Effects. 346-355
  
• François Pottier:
  Static Name Control for FreshML. 356-365
  
• Cristiano Calcagno, Peter W. O'Hearn, Hongseok Yang:
  Local Action and Abstract Separation Logic. 366-378
  

Game Semantics

• Russell Harmer, Martin Hyland, Paul-André Melliès:
  Categorical Combinatorics for Innocent Strategies. 379-388
  
• Paul-André Melliès, Nicolas Tabareau:
  Resource modalities in game semantics. 389-398
  
• Nikos Tzevelekos:
  Full abstraction for nominal general references. 399-410
  

Linear Logic

• Ulrich Schöpp:
  Stratified Bounded Affine Logic for Logarithmic Space. 411-420
  
• Patrick Baillot, Paolo Coppola, Ugo Dal Lago:
  Light Logics and Optimal Reduction: Completeness and Complexity. 421-430
  
• Paulo Oliva:
  Modified Realizability Interpretation of Classical Linear Logic. 431-442
  

Topology and Computable Mathematics

• Martín Hötzel Escardó:
  Infinite sets that admit fast exhaustive search. 443-452
  
• Jean Goubault-Larrecq:
  On Noetherian Spaces. 453-462
  
• Abbas Edalat:
  A computable approach to measure and integration theory. 463-472