CSDL - Proceedings L

Organizing Committee (PDF)

pp. xi-xii

Additional Reviewers (PDF)

pp. xiii

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

PDF

Strong Normalization as Safe Interaction (Abstract)

Colin Riba, INPL & LORIA, France

pp. 13-22

PDF

A Dependent Set Theory (Abstract)

Wojciech Moczydlowski, Cornell University, USA

pp. 23-34

PDF

Computational Proof Theory

Some Methods of Problem Solving in Elementary Geometry (Abstract)

Thomas C. Hales, University of Pittsburgh, USA

pp. 35-40

PDF

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

PDF

Complete Sequent Calculi for Induction and Infinite Descent (Abstract)

James Brotherston, Imperial College, London, UK

Alex Simpson, University of Edinburgh, UK

pp. 51-62

PDF

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

PDF

A Complete Axiomatization of Knowledge and Cryptography (Abstract)

Mika Cohen, KTH, Sweden

Mads Dam, KTH, Sweden

pp. 77-88

PDF

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

PDF

Game Relations and Metrics (Abstract)

Luca de Alfaro, University of California, Santa Cruz, USA

Rupak Majumdar, University of California, Los Angeles, USA

Vishwanath Raman, University of California, Santa Cruz, USA

Mari?lle Stoelinga, University of Twente, the Netherlands

pp. 99-108

PDF

The Cost of Punctuality (Abstract)

Patricia Bouyer, LSV, CNRS & ENS Cachan, France; Oxford University, UK

Nicolas Markey, LSV, CNRS & ENS Cachan, France

Jo?l Ouaknine, Oxford University, UK

James Worrell, Oxford University, UK

pp. 109-120

PDF

Verification

Two-way unary temporal logic over trees (Abstract)

Mikolaj Bojanczyk, Warsaw University

pp. 121-130

PDF

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

Marcin Jurdzinski, University of Warwick, UK

Ranko Lazic, University of Warwick, UK

pp. 131-140

PDF

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

PDF

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

Rajeev Alur, University of Pennsylvania

Marcelo Arenas, Pontificia Universidad Catolica de Chile

Pablo Barcel?, Universidad de Chile

Kousha Etessami, University of Edinburgh

Neil Immerman, University of Massachusetts

Leonid Libkin, University of Edinburgh

pp. 151-160

PDF

A Robust Class of Context-Sensitive Languages (Abstract)

Salvatore La Torre, Universita di Salerno, Italy

Parthasarathy Madhusudan, University of Illinois, USA

Gennaro Parlato, Universita di Salerno, Italy

pp. 161-170

PDF

A New Efficient Simulation Equivalence Algorithm (Abstract)

Francesco Ranzato, University of Padova, Italy

Francesco Tapparo, University of Padova, Italy

pp. 171-180

PDF

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

Detlef K?hler, University of Kiel, Germany

Ralf K?sters, ETH Zurich, Switzerland

Tomasz Truderung, Wroclaw University, Poland

pp. 181-192

PDF

Constraints

Symmetric Datalog and Constraint Satisfaction Problems in Logspace (Abstract)

L?szl? Egri, McGill University, Canada

Benoit Larose, Concordia University, Canada

Pascal Tesson, Laval University, Canada

pp. 193-202

PDF

Quantified Equality Constraints (Abstract)

Manuel Bodirsky, Humboldt-Universitat zu Berlin, Germany

Hubie Chen, Universitat Pompeu Fabra, Spain

pp. 203-212

PDF

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

Pawel Idziak, Jagiellonian University, Poland

Petar Markovic, University of Novi Sad, Serbia

Ralph McKenzie, Vanderbilt University, USA

Matthew Valeriote, McMaster University, Canada

Ross Willard, University of Waterloo, Canada

pp. 213-224

PDF

Proof Complexity

Examining The Fragments of G (Abstract)

Steven James Perron, University of Toronto, Canada

pp. 225-234

PDF

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

Phuong Nguyen, University of Toronto, Canada

pp. 235-244

PDF

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

PDF

Finite Model Theory

Reflections on Finite Model Theory (Abstract)

Phokion G. Kolaitis, IBM Almaden Research Center, USA

pp. 257-269

PDF

Locally Excluding a Minor (Abstract)

Anuj Dawar, University of Cambridge, UK

Martin Grohe, Humboldt Universitat zu Berlin, Germany

Stephan Kreutzer, Universitat zu Berlin, Germany

pp. 270-279

PDF

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

Balder ten Cate, Univ. of Amsterdam, the Netherlands

Johan van Benthem, Univ. of Amsterdam, the Netherlands

Jouko V??n?nen, Univ. of Amsterdam, the Netherlands

pp. 280-292

PDF

Concurrency and Process Calculi

Environmental Bisimulations for Higher-Order Languages (Abstract)

Davide Sangiorgi, University of Bologna, Italy

Naoki Kobayashi, Tohoku University, Japan

Eijiro Sumii, Tohoku University, Japan

pp. 293-302

PDF

Pi-Calculus in Logical Form (Abstract)

Marcello Bonsangue, Leiden University, the Netherlands

Alexander Kurz, University of Leicester, United Kingdom

pp. 303-312

PDF

Characterising Testing Preorders for Finite Probabilistic Processes (Abstract)

Yuxin Deng, Jiao tong University, China; University of New South Wales, Australia

Rob van Glabbeek, National ICT Australia; University of New South Wales, Australia

Matthew Hennessy, University of Sussex, UK

Carroll Morgan, University of New South Wales, Australia

Chenyi Zhang, National ICT Australia; University of New South Wales, Australia

pp. 313-325

PDF

Semantics of Programming Languages

Higher-Order Matching, Games and Automata (Abstract)

Colin Stirling, University of Edinburgh, UK

pp. 326-335

PDF

Bialgebraic Operational Semantics and Modal Logic (Abstract)

Bartek Klin, University of Edinburgh; Warsaw University

pp. 336-345

PDF

Relational Parametricity for Computational Effects (Abstract)

Rasmus Ejlers M?gelberg, University of Edinburgh, UK

Alex Simpson, University of Edinburgh, UK

pp. 346-355

PDF

Static Name Control for FreshML (Abstract)

Fran?ois Pottier, INRIA, France

pp. 356-365

PDF

Local Action and Abstract Separation Logic (Abstract)

Cristiano Calcagno, Imperial College, London, UK

Peter W. O'Hearn, Queen Mary, University of London

Hongseok Yang, Queen Mary, University of London

pp. 366-378

PDF

Game Semantics

Categorical Combinatorics for Innocent Strategies (Abstract)

Russ Harmer, Universite Paris 7, France

Martin Hyland, University of Cambridge, UK

Paul-Andr? Melli?s, Universite Paris 7, France

pp. 379-388

PDF

Resource modalities in game semantics (Abstract)

Paul-Andr? Melli?s, Universite Paris 7, France

Nicolas Tabareau, Universite Paris 7, France

pp. 389-398

PDF

Full abstraction for nominal general references (Abstract)

Nikos Tzevelekos, Oxford University

pp. 399-410

PDF

Linear Logic

Stratified Bounded Affine Logic for Logarithmic Space (Abstract)

Ulrich Sch?pp, Ludwig-Maximilians-Universitat Munchen, Germany

pp. 411-420

PDF

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

Patrick Baillot, LIPN, CNRS & Universite Paris Nord, France

Paolo Coppola, Universita di Udine, Italy

Ugo Dal Lago, Universita di Bologna, Italy

pp. 421-430

PDF

Modified Realizability Interpretation of Classical Linear Logic (Abstract)

Paulo Oliva, Queen Mary, University of London, UK

pp. 431-442

PDF

Topology and Computable Mathematics

Infinite sets that admit fast exhaustive search (Abstract)

Mart?n Escard?, University of Birmingham, UK

pp. 443-452

PDF

On Noetherian Spaces (Abstract)

Jean Goubault-Larrecq, LSV, ENS Cachan, CNRS, INRIA Futurs, France

pp. 453-462

PDF

A computable approach to measure and integration theory (Abstract)

Abbas Edalat, Imperial College London, UK

pp. 463-472

PDF

Author Index

Author Index (PDF)

pp. 473