Foreword |
Conference Organization |
Program Committee |
Additional Reviewers |
Proof Nets for Unit-Free Multiplicative-Additive Linear Logic / D. Hughes ; R. van GlabbeekSession 1: |
About Translations of Classical Logic into Polarized Linear Logic / O. Laurent ; L. Regnier |
System ST [beta]-Reduction and Completeness / C. Raffalli |
Invited Tutorial--Types and Programming Languages: The Next Generation / B. C. PierceSession 2: |
Reasoning about Hierarchical Storage / A. Ahmed ; L. Jia ; D. WalkerSession 3: |
Invited Talk--Formal Verification at Intel / J. Harrison |
New Directions in Instantiation-Based Theorem Proving / H. Ganzinger ; K. KorovinSession 4: |
Abstract Saturation-Based Inference / N. Dershowitz ; C. Kirchner |
Orienting Equalities with the Knuth-Bendix Order / A. Voronkov |
Practical Reflection in Nuprl / E. Barzilay ; S. Allen ; R. ConstableShort Presentations I: |
An Applicative-Order Term Rewriting System for Code Generation, and Its Termination Analysis / O. Kiselyov |
Patterns Based on Multiple Interacting Partial Orders / F. J. Oles |
Logic of Subtyping / P. Naumov |
A Language and a Notion of Truth for Cryptographic Properties / S. Kramer |
The Relative Complexity of Local Search Heuristics and the Iteration Principle / T. Morioka |
A Second-Order Theory for NL / S. Cook ; A. Kolokolova |
Dependent Intersection: A New Way of Defining Records in Type Theory / A. KopylovSession 5: |
Structural Subtyping of Non-Recursive Types Is Decidable / V. Kuncak ; M. Rinard |
On Program Equivalence in Languages with Ground-Type References / A. S. Murawski |
A Proof Theory for Generic Judgments: An Extended Abstract / D. Miller ; A. TiuSession 6: |
Polynomial-Time Algorithms from Ineffective Proofs / P. Oliva |
The Complexity of Resolution Refinements / J. Buresh-Oppenheim ; T. Pitassi |
Successor-Invariance in the Finite / B. RossmanSession 7: |
Invited Talk--Will Deflation Lead to Depletion? On Non-Monotone Fixed Point Inductions / E. Gradel ; S. Kreutzer |
On Automatic Partial Orders / B. Khoussainov ; S. Rubin ; F. StephanSession 8: |
Logical Definability and Query Languages over Unranked Trees / L. Libkin ; F. Neven |
Query Evaluation on Compressed Trees / M. Frick ; M. Grohe ; C. Koch |
Revisiting Digitization, Robustness, and Decidability for Timed Automata / J. Ouaknine ; J. WorrellSession 9: |
Satisfiability in Alternating-Time Temporal Logic / G. van Drimmelen |
Strong Bisimilarity on Basic Parallel Processes Is PSPACE-Complete / P. Jancar |
Invited Tutorial--Logic in Access Control / M. AbadiSession 10: |
The Planning Spectrum--One, Two, Three, Infinity / M. Pistore ; M. Y. VardiSession 11: |
Invited Talk--Advice about Logical AI / J. McCarthy |
A Sound Framework for Untrusted Verification-Condition Generators / G. C. Necula ; R. R. SchneckSession 12: |
An NP Decision Procedure for Protocol Insecurity with XOR / Y. Chevalier ; R. Kusters ; M. Rusinowitch ; M. Turuani |
Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or / H. Comon-Lundh ; V. Shmatikov |
Spectrum Hierarchies and Subdiagonal Functions / A. HunterSession 13: |
Spectra of Monadic Second-Order Formulas with One Unary Function / Y. Gurevich ; S. Shelah |
Convergence Law for Random Graphs with Specified Degree Sequence / J. F. Lynch |
Homomorphism Closed vs. Existential Positive / T. FederSession 14: |
Tractable Conservative Constraint Satisfaction Problems / A. A. Bulatov |
A Constraint-Based Presentation and Generalization of Rows / F. Pottier |
Labelled Markov Processes: Stronger and Faster Approximations / V. Danos ; J. DesharnaisSession 15: |
Invited Talk--Model Checking for Probability and Time: From Theory to Practice / M. Kwiatkowska |
Model Checking Guarded Protocols / E. A. Emerson ; V. KahlonSession 16: |
Model-Checking Trace Event Structures / P. Madhusudan |
Micro-Macro Stack Systems: A New Frontier of Elementary Decidability for Sequential Systems / N. Piterman |
A Proposal to Extend Abstract State Machines to Applications in Systems Biology / Short Presentations II: |
Stuttering Refinement on Partial Systems / S. Nejati ; A. Gurfinkel |
Assume-Guarantee Reasoning with Features / B. Devereux |
Modularity Theorems for Non-Monotone Induction / M. Denecker ; E. Ternovska |
Linear-Time Algorithms for Monadic Logic / S. Lindell |
Game-Based Notions of Locality / M. Arenas ; P. Barcelo |
Arb: An Implementation of Selecting Tree Automata for XML Query Processing |
Author Index |