Program

Friday, August 11th

Friday's program is also available side by side with other meetings.

19:00‑21:00  LICS Reception
Location: Grand Ballroom C

Saturday, August 12th

Saturday's program is also available with abstracts or side by side with other meetings.

08:45‑10:00  FLoC Opening and Plenary Session
Chair: Moshe Vardi, Thomas Ball, Wolfram Schulte, Rajeev Alur
Location: Grand Ballroom C

08:45	Introduction and Welcome
09:00	Randal E. Bryant (Carnegie Mellon University) Formal Verification of Infinite State Systems using Boolean Methods [ppt]

10:00‑10:30  Break

10:30‑12:30  Session 1: Complexity and Decidability
Chair: Stephan Kreutzer
Location: Grand Ballroom C

10:30	Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin and Claire David Two-Variable Logic on Words with Data
11:00	Stephane Demri and Ranko Lazic LTL with the Freeze Quantifier and Register Automata
11:30	Guoqiang Pan and Moshe Y. Vardi Fixed-Parameter Hierarchies inside PSPACE
12:00	Martin Otto The boundedness problem for monadic universal first-order logic

12:30‑14:00  Lunch break

14:00‑15:30  Session 2: Concurrency
Chair: Christel Baier
Location: Grand Ballroom C

14:00	Marcelo Fiore and Sam Staton A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics
14:30	Catuscia Palamidessi , Vijay Saraswat , Frank D. Valencia and Björn Victor On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi-Calculus
15:00	Filippo Bonchi , Ugo Montanari and Barbara König Saturated Semantics for Reactive Systems

15:30‑16:00  Break

16:00‑18:00  Session 3: Pushdown Systems
Chair: Mahesh Viswanathan
Location: Grand Ballroom C

16:00	Luke Ong On model-checking trees generated by higher-order recursion schemes
16:30	Dietrich Kuske and Markus Lohrey Monadic chain logic over iterations and applications to pushdown systems
17:00	Vineet Kahlon and Aarti Gupta An Automata-theoretic Appraoch for Model Checking Threads for LTL Properties
17:30	Tachio Terauchi and Alex Aiken On Typability for Rank-2 Intersection Types with Polymorphic Recursion

18:00‑19:00  LICS Business Meeting
Location: Grand Ballroom C

Sunday, August 13th

Sunday's program is also available with abstracts or side by side with other meetings.

09:00‑10:00  Invited Talk
Chair: Phokion Kolaitis
Location: Grand Ballroom C

09:00

Andreas Blass (University of Michigan, Ann Arbor) Adapting Logics [pdf]

10:00‑10:30  Break

10:30‑12:30  Session 4: Logics of Programs
Chair: Patrice Godefroid
Location: Grand Ballroom C

10:30	Adam Barth and John C. Mitchell Managing Digital Rights using Linear Logic
11:00	Matthew Parkinson , Richard Bornat and Cristiano Calcagno Variables as Resource in Hoare Logics
11:30	Jonathan Hayman and Glynn Winskel Independence and Concurrent Separation Logic
12:00	Daniel Leivant Matching explicit and modal reasoning about programs: a proof theoretic delineation of dynamic logic

12:30‑14:00  Lunch break

14:00‑15:30  Session 5: Proof Theory
Chair: Christel Baier
Location: Grand Ballroom C

14:00	Ugo Dal Lago Context Semantics, Linear Logic and Computational Complexity
14:30	Olivier Laurent and Lorenzo Tortora de Falco Obsessional cliques: a semantic characterization of bounded time complexity
15:00	Alexis Maciel and Toniann Pitassi A Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives

15:30‑16:00  Break

16:00‑18:00  Session 6: Model Theory
Chair: Moshe Vardi
Location: Grand Ballroom C

16:00	Benoit Larose , Cynthia Loten and Claude Tardif A Characterisation of First-Order Constraint Satisfaction Problems
16:30	Laura Chaubard, Jean-Eric Pin and Howard Straubing First order formulas with modular predicates
17:00	Emil Kiss and Matthew Valeriote On tractability and congruence distributivity
17:30	Lutz Schröder and Dirk Pattinson PSPACE bounds for rank-1 modal logics

19:00‑22:00  LICS-SAT-RTA Joint Banquet
Location: Grand Ballroom B

Monday, August 14th

Monday's program is also available with abstracts or side by side with other meetings.

09:00‑10:00  Invited Talk
Chair: Patrice Godefroid
Location: Metropolitan A

09:00

Orna Kupferman (Hebrew University, Israel) Avoiding Determinization [ppt]

10:00‑10:30  Break

10:30‑12:30  Session 7: Temporal Logics and Automata
Chair: Rajeev Alur
Location: Metropolitan A

10:30	Nir Piterman From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata
11:00	Orna Kupferman and Moshe Y. Vardi Memoryful Branching-Time Logic
11:30	Nir Piterman and Amir Pnueli Faster Solutions of Street and Rabin Games
12:00	Mikolaj Bojanczyk and Thomas Colcombet Bounds in omega-regularity

12:30‑14:00  Lunch break

14:00‑16:00  Session 8: Lambda Calculus
Chair: Radha Jagadeesan
Location: Metropolitan A

14:00	Soren Lassen Head normal form bisimulation for pairs and the lambda-mu calculus
14:30	Thierry Coquand and Arnaud Spiwack Proof of strong normalisation using domain theory
15:00	Giulio Manzonetto and Antonino Salibra Boolean algebras for lambda calculus
15:30	Makoto Tatsuta and Mariangiola Dezani Normalisation is insensible to lambda-term identity or difference

16:00‑16:30  Break

16:30‑18:00  Keynote Session: Marking the Gödel Centenary
Chair: Wolfram Schulte, Moshe Vardi
Location: Metropolitan A and B

16:30	John Dawson (Penn State, York Campus) Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science [ppt]
17:15	Dana Scott (Carnegie Mellon University) The Future of Proof [pdf]

Tuesday, August 15th

Tuesday's program is also available with abstracts or side by side with other meetings.

09:00‑10:00  Invited Talk
Chair: Radha Jagadeesan
Location: Metropolitan A

09:00

Andy Gordon (Microsoft Research) Provable Implementations of Security Protocols [ppt]

10:00‑10:30  Break

10:30‑12:00  Session 9: Timed and Stochastic Systems
Chair: Mahesh Viswanathan
Location: Metropolitan A

10:30	Tomas Brazdil, Vaclav Brozek, Vojtech Forejt and Antonin Kucera Stochastic Games with Branching-Time Winning Objectives
11:00	Dexter Kozen Coinductive Proof Principles for Stochastic Processes
11:30	Patricia Bouyer , Thomas Brihaye and Fabrice Chevalier Control in o-minimal hybrid systems

12:00‑12:30  Session 10: Short Presentations 1
Chair: Mahesh Viswanathan
Location: Metropolitan A

12:00	Murray Patterson , Yongmei Liu, Eugenia Ternovska and Arvind Gupta Grounding for Model Expansion in k-Guarded Formulas
12:10	Jørgen Villadsen Nominalization in Intensional Type Theory
12:20	Leona F. Fass A Logical Look at Agents’ Problem-Solving on the Semantic Web

12:30‑14:00  Lunch break

14:00‑15:30  Session 11: Verification
Chair: Stephan Kreutzer
Location: Metropolitan A

14:00	Thomas Ball and Orna Kupferman An Abstraction-Refinement Framework for Multi-Agent Systems
14:30	Daniele Varacca and Hagen Voelzer Temporal logics and model checking for fairly correct systems
15:00	Sharon Shoham and Orna Grumberg 3-Valued Abstraction: More Precision at Less Cost

15:30‑16:00  Break

16:00‑17:00  Session 12: Approximations
Chair: Victor Dalmau
Location: Metropolitan A

16:00	Anuj Dawar, Martin Grohe, Stephan Kreutzer and Nicole Schweikardt Approximation Schemes for First-Order Definable Optimization Problems
16:30	Eldar Fischer , Frederic Magniez and Michel de Rougemont Approximate Satisfiability and Equivalence

17:00‑17:40  Session 13: Short Presentations 2
Chair: Victor Dalmau
Location: Metropolitan A

17:00	Julian Zinn and Rakesh Verma A Polynomial-time Algorithm for Uniqueness of Normal Forms of Linear Shallow Term Rewrite Systems
17:10	Aaron Hunter Non-Closure Results for First-Order Spectra
17:20	Detlef Kaehler, Ralf Kuesters and Thomas Wilke A Dolev-Yao-based Definition of Abuse-free Protocols
17:30	Guillaume Burel and Claude Kirchner An Abstract Completion Procedure for Cut Elimination in Deduction Modulo