| Foreword |
| Conference Organisers |
| Programme Committee |
| Additional Reviewers |
| FLoC Joint Invited Lecture |
| Little Engines of Proof / N. Shankar |
| Automatic Decidability / C. Lynch ; B. MorawskaSession 1： |
| Tree-Like Counterexamples in Model Checking / E. Clarke ; S. Jha ; Y. Lu ; H. VeithSession 2： |
| Probabilistic Abstraction for Model Checking: An Approach Based on Property Testing / S. Laplante ; R. Lassaigne ; F. Magniez ; S. Peyronnet ; M. de Rougemont |
| Semantic Minimization of 3-Valued Propositional Formulae / T. Reps ; A. Loginov ; M. Sagiv |
| Invited Lecture: Separation Logic: A Logic for Shared Mutable Data Structures / J. C. ReynoldsSession 3： |
| A Stratified Semantics of General References Embeddable in Higher-Order Logic / A. J. Ahmed ; A. W. Appel ; R. Virga |
| A Syntactic Approach to Foundational Proof-Carrying Code / N. A. Hamid ; Z. Shao ; V. Trifonov ; S. Monnier ; Z. NiSession 4： |
| A Fully Abstract May Testing Semantics for Concurrent Objects / A. Jeffrey ; J. Rathke |
| Semantics and Logic of Object Calculi / B. Reus ; T. Streicher |
| Efficient Type Inference for Record Concatenation and Subtyping / J. Palsberg ; T. ZhaoSession 5： |
| Semantic Subtyping / A. Frisch ; G. Castagna ; V. Benzaken |
| Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types / M. Fiore ; R. Di Cosmo ; V. Balat |
| On the Lambda Y Calculus / R. StatmanSession 6： |
| Dense Real-Time Games / M. Faella ; S. La Torre ; A. Murano |
| Computing Reachability Relations in Timed Automata / C. Dima |
| Invited Lecture: Monadic Queries over Tree-Structured Data / G. Gottlob ; C. KochSession 7： |
| Tree Extension Algebras: Logics, Automata, and Query Languages / M. Benedikt ; L. Libkin |
| The Complexity of First-Order and Monadic Second-Order Logic Revisited / M. Frick ; M. GroheSession 8： |
| The 0-1 Law Fails for Frame Satisfiability of Propositional Modal Logic / J.-M. Le Bars |
| Some Results on Automatic Structures / H. Ishihara ; B. Khoussainov ; S. Rubin |
| Observational Equivalence of 3rd-Order Idealized Algol is Decidable / C.-H. L. OngSession 9： |
| Games on Graphs and Sequentially Realizable Functionals / M. Hyland ; A. Schalk |
| Polarized Games / O. Laurent |
| Domain Theory and Differential Calculus (Functions of One Variable) / A. Edalat ; A. LieutierSession 10： |
| Computational Adequacy for Recursive Types in Models of Intuitionistic Set Theory / A. Simpson |
| The Powerdomain of Indexed Valuations / D. Varacca |
| Invited Lecture: Complexity Classes, Propositional Proof Systems, and Formal Theories / S. A. CookSession 11： |
| Complete Problems for Dynamic Complexity Classes / W. Hesse ; N. Immerman |
| Unsatisfiable Random Formulas Are Hard to Certify / A. AtseriasSession 12： |
| The Proof Complexity of Linear Algebra / M. Soltys ; S. Cook |
| Calibrating Computational Feasibility by Abstraction Rank / D. Leivant |
| Short Presentations / Session 13： |
| Lessons Learned from Formal Developments in PVS / J. Ford ; I. A. Mason |
| CLP Implementation of a Phase Model Checker / S. Soliman |
| An Overview of MR, a Calculus of Mobile Resources / J. C. Godskesen ; T. Hildebrandt ; V. Sassone |
| Ludics Dynamics: Designs and Interactive Observability / C. Faggian |
| Invited Tutorial: Description Logics: Foundations for Class-Based Knowledge Representation / D. Calvanese ; G. De Giacomo ; M. LenzeriniSession 14： |
| Modal and Guarded Characterisation Theorems over Finite Transition Systems / M. Otto |
| Temporal Logic with Forgettable Past / F. Laroussinie ; N. Markey ; P. SchnoebelenSession 15： |
| Decidable and Undecidable Fragments of First-Order Branching Temporal Logics / I. Hodkinson ; F. Wolter ; M. Zakharyaschev |
| Expressive Equivalence of Least and Inflationary Fixed-Point Logic / S. Kreutzer |
| The Metric Analogue of Weak Bisimulation for Probabilistic Processes / J. Desharnais ; R. Jagadeesan ; V. Gupta ; P. PanangadenSession 16： |
| Separability, Expressiveness, and Decidability in the Ambient Logic / D. Hirschkoff ; E. Lozes ; D. Sangiorgi |
| Linearity in Process Languages / M. Nygaard ; G. Winskel |
| Deciding Confluence of Certain Term Rewriting Systems in Polynomial Time / A. TiwariSession 17： |
| Two Adversary Lower Bounds for Parity Games / H. Bjorklund ; S. Vorobyov |
| Is Randomized Gurvich-Karzanov-Khachiyan's Algorithm for Parity Games Polynomial? / E. Beffara |
| Time-Space Computational Complexity of Imperative Programming Languages / E. Covino ; G. Pani |
| Author Index |
| Foreword |
| Conference Organisers |
| Programme Committee |
| Additional Reviewers |
| FLoC Joint Invited Lecture |
| Little Engines of Proof / N. Shankar |
