The Community for Technology Leaders
Logic in Computer Science, Symposium on (2007)
Wroclaw, Poland
July 10, 2007 to July 14, 2007
ISSN: 1043-6871
ISBN: 0-7695-2908-9
TABLE OF CONTENTS

Foreword (PDF)

pp. ix-x
Introduction

Foreword (PDF)

pp. ix-x

Organizing Committee (PDF)

pp. xi-xii
Type Theory

Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements (Abstract)

Andreas Abel , Ludwig-Maximilians-Universitat, Germany
Thierry Coquand , Chalmers University of Technology, Sweden
Peter Dybjer , Chalmers University of Technology, Sweden
pp. 3-12

Strong Normalization as Safe Interaction (Abstract)

Colin Riba , INPL & LORIA, France
pp. 13-22

A Dependent Set Theory (Abstract)

Wojciech Moczydlowski , Cornell University, USA
pp. 23-34
Computational Proof Theory

Some Methods of Problem Solving in Elementary Geometry (Abstract)

Thomas C. Hales , University of Pittsburgh, USA
pp. 35-40

Principles of Superdeduction (Abstract)

Paul Brauner , INPL & LORIA, France
Cl?ment Houtmann , ENS de Cachan & LORIA, France
Claude Kirchner , INRIA & LORIA, France
pp. 41-50

Complete Sequent Calculi for Induction and Infinite Descent (Abstract)

Alex Simpson , University of Edinburgh, UK
James Brotherston , Imperial College, London, UK
pp. 51-62
Security

Highly Efficient Secrecy-Preserving Proofs of Correctness of Computations and Applications (Abstract)

Michael O. Rabin , Harvard University, USA
Rocco A. Servedio , Columbia University, USA
Christopher Thorpe , Harvard University, USA
pp. 63-76
Timed and Stochastic Systems

Limits of Multi-Discounted Markov Decision Processes (Abstract)

Hugo Gimbert , LIX, Ecole Polytechnique, France
Wieslaw Zielonka , Universite Denis Diderot, France
pp. 89-98

Game Relations and Metrics (Abstract)

Rupak Majumdar , University of California, Los Angeles, USA
Luca de Alfaro , University of California, Santa Cruz, USA
Mari?lle Stoelinga , University of Twente, the Netherlands
Vishwanath Raman , University of California, Santa Cruz, USA
pp. 99-108

The Cost of Punctuality (Abstract)

Patricia Bouyer , LSV, CNRS & ENS Cachan, France; Oxford University, UK
Nicolas Markey , LSV, CNRS & ENS Cachan, France
James Worrell , Oxford University, UK
Jo?l Ouaknine , Oxford University, UK
pp. 109-120
Verification

Two-way unary temporal logic over trees (Abstract)

Mikolaj Bojanczyk , Warsaw University
pp. 121-130

Alternation-free modal mu-calculus for data trees (Abstract)

Ranko Lazic , University of Warwick, UK
Marcin Jurdzinski , University of Warwick, UK
pp. 131-140

A Contraction Method to Decide MSO Theories of Deterministic Trees (Abstract)

Angelo Montanari , Universita di Udine, Italy
Gabriele Puppis , Universita di Udine, Italy
pp. 141-150

First-Order and Temporal Logics for Nested Words (Abstract)

Rajeev Alur , University of Pennsylvania
Leonid Libkin , University of Edinburgh
Kousha Etessami , University of Edinburgh
Marcelo Arenas , Pontificia Universidad Catolica de Chile
Neil Immerman , University of Massachusetts
Pablo Barcel? , Universidad de Chile
pp. 151-160

A Robust Class of Context-Sensitive Languages (Abstract)

Parthasarathy Madhusudan , University of Illinois, USA
Gennaro Parlato , Universita di Salerno, Italy
Salvatore La Torre , Universita di Salerno, Italy
pp. 161-170

A New Efficient Simulation Equivalence Algorithm (Abstract)

Francesco Ranzato , University of Padova, Italy
Francesco Tapparo , University of Padova, Italy
pp. 171-180

Infinite State AMC-Model Checking for Cryptographic Protocols (Abstract)

Tomasz Truderung , Wroclaw University, Poland
Detlef K?hler , University of Kiel, Germany
Ralf K?sters , ETH Zurich, Switzerland
pp. 181-192
Constraints

Symmetric Datalog and Constraint Satisfaction Problems in Logspace (Abstract)

L?szl? Egri , McGill University, Canada
Pascal Tesson , Laval University, Canada
Benoit Larose , Concordia University, Canada
pp. 193-202
Constraints

Tractability and learnability arising from algebras with few subpowers (Abstract)

Petar Markovic , University of Novi Sad, Serbia
Matthew Valeriote , McMaster University, Canada
Ralph McKenzie , Vanderbilt University, USA
Ross Willard , University of Waterloo, Canada
Pawel Idziak , Jagiellonian University, Poland
pp. 213-224
Proof Complexity

Examining The Fragments of G (Abstract)

Steven James Perron , University of Toronto, Canada
pp. 225-234

Separating DAG-Like and Tree-Like Proof Systems (Abstract)

Phuong Nguyen , University of Toronto, Canada
pp. 235-244

The Complexity of Proving the Discrete Jordan Curve Theorem (Abstract)

Phuong Nguyen , University of Toronto, Canada
Stephen A. Cook , University of Toronto, Canada
pp. 245-256
Finite Model Theory

Reflections on Finite Model Theory (Abstract)

Phokion G. Kolaitis , IBM Almaden Research Center, USA
pp. 257-269

Locally Excluding a Minor (Abstract)

Martin Grohe , Humboldt Universitat zu Berlin, Germany
Stephan Kreutzer , Universitat zu Berlin, Germany
Anuj Dawar , University of Cambridge, UK
pp. 270-279

Lindstrom theorems for fragments of first-order logic (Abstract)

Balder ten Cate , Univ. of Amsterdam, the Netherlands
Jouko V??n?nen , Univ. of Amsterdam, the Netherlands
Johan van Benthem , Univ. of Amsterdam, the Netherlands
pp. 280-292
Concurrency and Process Calculi

Environmental Bisimulations for Higher-Order Languages (Abstract)

Naoki Kobayashi , Tohoku University, Japan
Davide Sangiorgi , University of Bologna, Italy
Eijiro Sumii , Tohoku University, Japan
pp. 293-302

Pi-Calculus in Logical Form (Abstract)

Alexander Kurz , University of Leicester, United Kingdom
Marcello Bonsangue , Leiden University, the Netherlands
pp. 303-312

Characterising Testing Preorders for Finite Probabilistic Processes (Abstract)

Chenyi Zhang , National ICT Australia; University of New South Wales, Australia
Yuxin Deng , Jiao tong University, China; University of New South Wales, Australia
Matthew Hennessy , University of Sussex, UK
Rob van Glabbeek , National ICT Australia; University of New South Wales, Australia
Carroll Morgan , University of New South Wales, Australia
pp. 313-325
Semantics of Programming Languages

Higher-Order Matching, Games and Automata (Abstract)

Colin Stirling , University of Edinburgh, UK
pp. 326-335

Bialgebraic Operational Semantics and Modal Logic (Abstract)

Bartek Klin , University of Edinburgh; Warsaw University
pp. 336-345

Relational Parametricity for Computational Effects (Abstract)

Alex Simpson , University of Edinburgh, UK
Rasmus Ejlers M?gelberg , University of Edinburgh, UK
pp. 346-355

Static Name Control for FreshML (Abstract)

Fran?ois Pottier , INRIA, France
pp. 356-365

Local Action and Abstract Separation Logic (Abstract)

Hongseok Yang , Queen Mary, University of London
Cristiano Calcagno , Imperial College, London, UK
Peter W. O'Hearn , Queen Mary, University of London
pp. 366-378
Game Semantics

Categorical Combinatorics for Innocent Strategies (Abstract)

Martin Hyland , University of Cambridge, UK
Paul-Andr? Melli?s , Universite Paris 7, France
Russ Harmer , Universite Paris 7, France
pp. 379-388

Resource modalities in game semantics (Abstract)

Paul-Andr? Melli?s , Universite Paris 7, France
Nicolas Tabareau , Universite Paris 7, France
pp. 389-398
Linear Logic

Stratified Bounded Affine Logic for Logarithmic Space (Abstract)

Ulrich Sch?pp , Ludwig-Maximilians-Universitat Munchen, Germany
pp. 411-420

Light Logics and Optimal Reduction: Completeness and Complexity (Abstract)

Ugo Dal Lago , Universita di Bologna, Italy
Paolo Coppola , Universita di Udine, Italy
Patrick Baillot , LIPN, CNRS & Universite Paris Nord, France
pp. 421-430

Modified Realizability Interpretation of Classical Linear Logic (Abstract)

Paulo Oliva , Queen Mary, University of London, UK
pp. 431-442
Topology and Computable Mathematics

Infinite sets that admit fast exhaustive search (Abstract)

Mart?n Escard? , University of Birmingham, UK
pp. 443-452

On Noetherian Spaces (Abstract)

Jean Goubault-Larrecq , LSV, ENS Cachan, CNRS, INRIA Futurs, France
pp. 453-462

A computable approach to measure and integration theory (Abstract)

Abbas Edalat , Imperial College London, UK
pp. 463-472
Author Index

Author Index (PDF)

pp. 473
96 ms
(Ver )