Foreword

Conference Organisers (PDF)

pp. x

Programme Committee (PDF)

pp. xi

Additional Reviewers (PDF)

pp. xii

FLoC Joint Invited Lecture

Little Engines of Proof (PDF)

Natarajan Shankar, SRI International

pp. 3

Session 1

Automatic Decidability (Abstract)

Christopher Lynch, Clarkson University

Barbara Morawska, Clarkson University

pp. 7

PDF

Session 2

Tree-Like Counterexamples in Model Checking (Abstract)

Edmund Clarke, Carnegie Mellon University

Somesh Jha, University of Wisconsin

Yuan Lu, Broadcom COM

Helmut Veith, Technische Universität Wien

pp. 19

PDF

Probabilistic Abstraction for Model Checking: An Approach Based on Property Testing (Abstract)

Sophie Laplante, University of Paris-Sud

Richard Lassaigne, University of Paris 7

Frédéric Magniez, CNRS-LRI

Sylvain Peyronnet, University of Paris-Sud

Michel de Rougemont, University of Paris II

pp. 30

PDF

Semantic Minimization of 3-Valued Propositional Formulae (Abstract)

Thomas Reps, University of Wisconsin

Alexey Loginov, University of Wisconsin

Mooly Sagiv, Tel-Aviv University

pp. 40

PDF

Session 3

Separation Logic: A Logic for Shared Mutable Data Structures (Abstract)

John C. Reynolds, Carnegie Mellon University

pp. 55

PDF

A Stratified Semantics of General References Embeddable in Higher-Order Logic (Abstract)

Amal J. Ahmed, Princeton University

Andrew W. Appel, Princeton University

Roberto Virga, Princeton University

pp. 75

PDF

Session 4

A Syntactic Approach to Foundational Proof-Carrying Code (Abstract)

Nadeem A. Hamid, Yale University

Zhong Shao, Yale University

Valery Trifonov, Yale University

Stefan Monnier, Yale University

Zhaozhong Ni, Yale University

pp. 89

PDF

A Fully Abstract May Testing Semantics for Concurrent Objects (Abstract)

Alan Jeffrey, DePaul University

Julian Rathke, University of Sussex

pp. 101

PDF

Semantics and Logic of Object Calculi (Abstract)

Bernhard Reus, University of Sussex

Thomas Streicher, Technical University Darmstadt

pp. 113

PDF

Session 5

Efficient Type Inference for Record Concatenation and Subtyping (Abstract)

Jens Palsberg, Purdue University

Tian Zhao, Purdue University

pp. 125

PDF

Semantic Subtyping (Abstract)

Alain Frisch, École Normale Supérieure

Giuseppe Castagna, École Normale Supérieure

Véronique Benzaken, Université Paris-Sud

pp. 137

PDF

Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types (Abstract)

Marcelo Fiore, University of Cambridge

Roberto Di Cosmo, Université Paris 7 and INRIA-Roquencourt

Vincent Balat, Université Paris 7

pp. 147

PDF

Session 6

On The Lambda Y Calculus (Abstract)

Rick Statman, Carnegie Mellon University

pp. 159

PDF

Dense Real-Time Games (Abstract)

Marco Faella, Università degli Studi di Salerno

Salvatore La Torre, Università degli Studi di Salerno and University of Pennsylvania

Aniello Murano, Università degli Studi di Salerno and Rice University

pp. 167

PDF

Computing Reachability Relations in Timed Automata (Abstract)

Cătălin Dima, Verimag

pp. 177

PDF

Session 7

Monadic Queries over Tree-Structured Data (Abstract)

Georg Gottlob, Technische Universität Wien

Christoph Koch, Technische Universität Wien

pp. 189

PDF

Tree Extension Algebras: Logics, Automata, and Query Languages (Abstract)

Michael Benedikt, Bell Labs

Leonid Libkin, University of Toronto

pp. 203

PDF

Session 8

The Complexity of First-Order and Monadic Second-Order Logic Revisited (Abstract)

Markus Frick, University of Edinburgh

Martin Grohe, University of Edinburgh

pp. 215

PDF

The 0-1 law fails for frame satisfiability of propositional modal logic (Abstract)

Jean-Marie Le Bars, University of Caen

pp. 225

PDF

Some Results on Automatic Structures (Abstract)

Hajime Ishihara, Japan Advanced Institute of Science and Technology

Bakhadyr Khoussainov, University of Auckland

Sasha Rubin, University of Auckland

pp. 235

PDF

Session 9

Observational Equivalence of 3rd-Order Idealized Algol is Decidable (Abstract)

C.-H.L. Ong, Oxford University

pp. 245

PDF

Games on Graphs and Sequentially Realizable Functionals Extended Abstract (Abstract)

Martin Hyland, DPMMS

Andrea Schalk, University of Manchester

pp. 257

PDF

Polarized Games (Abstract)

Olivier Laurent, CNRS and University Paris 7

pp. 265

PDF

Session 10

Domain Theory and Differential Calculus (Functions of one Variable) (Abstract)

Abbas Edalat, Imperial College

André Lieutier, LMC/IMAG

pp. 277

PDF

Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory (Abstract)

Alex Simpson, University of Edinburgh

pp. 287

PDF

The Powerdomain of Indexed Valuations (Abstract)

Daniele Varacca, University of Aarhus and University of Cambridge

pp. 299

PDF

Session 11

Complexity Classes, Propositional Proof Systems, and Formal Theories (PDF)

Stephen A. Cook, University of Toronto

pp. 311

Complete Problems for Dynamic Complexity Classes (Abstract)

William Hesse, University of Massachusetts at Amherst

Neil Immerman, University of Massachusetts at Amherst

pp. 313

PDF

Session 12

Unsatisfiable Random Formulas Are Hard to Certify (Abstract)

Albert Atserias, Universitat Politècnica de Catalunya

pp. 325

PDF

The Proof Complexity of Linear Algebra (Abstract)

Michael Soltys, McMaster University

Stephen Cook, University of Toronto

pp. 335

PDF

Calibrating Computational Feasibility by Abstraction Rank (Abstract)

Daniel Leivant, Indiana University

pp. 345

PDF

Short Presentations

Lessons Learned from Formal Developments in PVS

CLP Implementation of a Phase Model Checker

An Overview of MR, a Calculus of Mobile Resources

Ludics Dynamics: Designs and Interactive Observability

Session 14

Description Logics: Foundations for Class-based Knowledge Representation (Abstract)

Diego Calvanese, Università di Roma "La Sapienza"

Giuseppe De Giacomo, Università di Roma "La Sapienza"

Maurizio Lenzerini, Università di Roma "La Sapienza"

pp. 359

PDF

Modal and Guarded Characterisation Theorems over Finite Transition Systems (Abstract)

Martin Otto, University of Wales Swansea

pp. 371

PDF

Session 15

Temporal Logic with Forgettable Past (Abstract)

François Laroussinie, ENS de Cachan & CNRS UMR

Nicolas Markey, ENS de Cachan & CNRS UMR and Université Orléans & CNRS

Philippe Schnoebelen, ENS de Cachan & CNRS UMR

pp. 383

PDF

Decidable and Undecidable Fragments of First-Order Branching Temporal Logics (Abstract)

Ian Hodkinson, Imperial College

Frank Wolter, Universität Leipzig

Michael Zakharyaschev, King?s College

pp. 393

PDF

Expressive Equivalence of Least and Inflationary Fixed-Point Logic (Abstract)

Stephan Kreutzer, RWTH Aachen

pp. 403

PDF

Session 16

The Metric Analogue of Weak Bisimulation for Probabilistic Processes (Abstract)

Josée Desharnais, Université Laval

Radha Jagadeesan, Loyola University-Lake Shore Campus

Vineet Gupta, Stratify Inc.

Prakash Panangaden, McGill University

pp. 413

PDF

Separability, Expressiveness, and Decidability in the Ambient Logic (Abstract)

Daniel Hirschkoff, LIP - ENS Lyon

Étienne Lozes, LIP - ENS Lyon

Davide Sangiorgi, INRIA

pp. 423

PDF

Linearity in Process Languages (Abstract)

Mikkel Nygaard, University of Aarhus

Glynn Winskel, University of Cambridge

pp. 433

PDF

Session 17

Deciding Confluence of Certain Term Rewriting Systems in Polynomial Time (Abstract)

Ashish Tiwari, SRI International

pp. 447

PDF

Two Adversary Lower Bounds for Parity Games

Is Randomized Gurvich-Karzanov-Khachiyan's Algorithm for Parity Games Polynomial?

Time-Space Computational Complexity of Imperative Programming Languages

Author Index

Author Index (PDF)

pp. 461