LICS 2003 Program ================= Sunday, June 22, 2003 9:00-10:30 Session 1: Chair: Philip Scott Opening Remarks Samson Abramsky, LICS General Chair Proof nets for unit-free multiplicative-additive linear logic Dominic Hughes and Rob van Glabbeek About Translations of Classical Logic into Polarized Linear Logic Olivier Laurent and Laurent Regnier System ST beta-reduction and completeness Christophe Raffalli 10:30-11:00 Coffee Break 11:00-12:30 Session 2: Chair: Luke Ong Invited Tutorial "Types and Programming Languages: The Next Generation" Benjamin Pierce 12:30-2:00 Lunch 2:00-3:30 Session 3: Chair: Frank Pfenning Reasoning about Hierarchical Storage Amal Ahmed, Limin Jia, and David Walker Invited Talk: "Formal verification at Intel" John Harrison 3:30-4:00 Coffee Break 4:00-5:30 Session 4: Chair: Paul-Andre Mellies New directions in instantiation-based theorem proving Harald Ganzinger and Konstantin Korovin Abstract Saturation-Based Inference Nachum Dershowitz and Claude Kirchner Orientability of systems of equations Konstantin Korovin and Andrei Voronkov 6:00-7:00 Short Presentations - Session 1: Chair: Philip Scott Practical Reflection in Nuprl Eli Barzilay, Stuart Allen, and Robert Constable An applicative-order term rewriting system for code generation, and its termination analysis Oleg Kiselyov Patterns Based on Multiple Interacting Partial Orders Frank J. Oles Logic of Subtyping Pavel Naumov A Language and a Notion of Truth for Cryptographic Properties Simon Kramer The Relative Complexity of Local Search Heuristics and the Iteration Principle Tsuyoshi Morioka A second-order theory for NL Stephen Cook and Antonina Kolokolova ======================================================== Monday, June 23, 2003 9:00-10:30 Session 5: Chair: Marcelo Fiore Dependent Intersection: A New Way of Defining Records in Type Theory Alexei Kopylov Structural Subtyping Non-Recursive Types is Decidable Viktor Kuncak and Martin Rinard On program equivalence in languages with ground-type references Andrzej S. Murawski 10:30-11:00 Coffee Break 11:00-12:30 Session 6: Chair: Amy Felty A Proof Theory for Generic Judgments Dale Miller and Alwen Tiu Polynomial-time algorithms from ineffective proofs Paulo Oliva The Complexity of Resolution Refinements Joshua Buresh-Oppenheim and Toniann Pitassi 12:30-2:00 Lunch 2:00-3:30 Session 7: Chair: Phokion Kolaitis Successor-Invariance in the Finite Benjamin Rossman Invited Talk "Will deflation lead to depletion? On non-monotone fixed point inductions" Erich Graedel 3:30-4:00 Coffee Break 4:00-5:30 Session 8: Chair: Martin Otto Automatic Partial Orders Bakhadyr Khoussainov, Sasha Rubin, and Frank Stephan Logical Definability and Query Languages over Unranked Trees Leonid Libkin and Frank Neven Query Evaluation on Compressed Trees Markus Frick, Martin Grohe and Christoph Koch 5:45-7:15 LICS 2003 Business Meeting ========================================================== Tuesday, June 24, 2003 9:00-10:30 Session 9: Chair: Martin Otto Revisiting Digitization, Robustness, and Decidability for Timed Automata Joel Ouaknine and James Worrell Satisfiability in Alternating-time Temporal Logic Govert van Drimmelen Bisimilarity on Basic Parallel Processes is PSPACE-complete Petr Jancar 10:30-11:00 Coffee Break 11:00-12:30 Session 10: Chair: Samson Abramsky Invited Tutorial "Logic in Access Control" Martin Abadi 12:30-2:00 Lunch 2:00-3:30 Session 11: Chair: Prakash Panangaden The Planning Spectrum - One, Two, Three, Infinity Marco Pistore and Moshe Y. Vardi Invited Talk "Advice about Logical AI" John McCarthy 3:30-4:00 Coffee Break 4:00-5:15 Session 12: Chair: Alan Jeffrey A Sound Framework for Untrusted Verification-Condition Generators George C. Necula and Robert R. Schneck An NP Decision Procedure for Protocol Insecurity with XOR Yannick Chevalier, Ralf Kuester, Michael Rusinowitch, and Mathieu Turuani "Intruder Deductions, Constraint Solving and Insecurity Decision in presence of exclusive or" Hubert Comon-Lundh and Vitaly Shmatikov 7:00- LICS 2003 Banquet ========================================================== Wednesday, June 25, 2003 9:00-10:30 Session 13: Chair: Andreas Blass Spectrum Hierarchies and Subdiagonal Functions Aaron Hunter Spectra of Monadic Second-Order Formulas with One Unary Function Yuri Gurevich and Saharon Shelah Convergence Law for Random Graphs with Specified Degree Sequence James F. Lynch 10:30-11:00 Coffee Break 11:00-12:30 Session 14: Chair: Phokion Kolaitis Homomorphism Closed vs. Existential Positive Tomas Feder and Moshe Y. Vardi Tractable Conservative Constraint Satisfaction Problems Andrei A. Bulatov A Constraint-Based Presentation and Generalization of Rows Francois Pottier 12:30-2:00 Lunch 2:00-3:30 Session 15: Chair: Ursula Martin Labelled Markov Processes: Stronger and Faster Approximations Vincent Danos and Josee Desharnais Invited Talk "Model checking for probability and time: from theory to practice" Marta Z. Kwiatkowska 3:30-4:00 Coffee Break 4:00-5:30 Session 16: Chair: Alan Jeffrey Model Checking Guarded Protocols E. Allen Emerson and Vineet Kahlon Model-checking Trace Event Structures P. Madhusudan Micro-Macro Stack Systems -- A New Frontier of Decidability for Sequential Systems Nir Piterman and Moshe Y. Vardi 6:00-7:00 Short Presentations - Session 2: Chair: Andreas Blass A Proposal to Extend Abstract State Machines to Applications in Systems Biology James F. Lynch Stuttering Refinement on Partial Systems Shiva Nejati and Arie Gurfinkel Assume-Guarantee Reasoning with Features Benet Devereux Modularity Theorems for Non-Monotone Induction Marc Denecker and Eugenia Ternovska Linear-time algorithms for Monadic Logic Steven Lindell Game-based Notions of Locality Marcelo Arenas, Pablo Barcelo, and Leonid Libkin Arb: An Implementation of Selecting Tree Automata for XML Query Processing Martin Grohe, Christoph Koch