LICS program

Sessions take place in auditorium 1 unless otherwise indicated.

Monday July 22nd

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

08:45-09:55  FLoC opening (joint with FME, RTA)
Chair: Moshe Vardi

08:45  Introduction and welcome
08:55  Natarajan Shankar, SRI International, USA
Invited talk: Little engines of proof

10:00-10:35  Session 1
Chair: Gordon Plotkin

10:00  Welcome to LICS by Samson Abramsky
10:05  Christopher Lynch and Barbara Morawska, Clarkson U, USA
Automatic decidability

10:35-11:00  Refreshments

11:00-12:30  Session 2
Chair: Leonid Libkin

11:00  Edmund M. Clarke, Carnegie Mellon U, USA; Somesh Jha, U Wisconsin-Madison, USA; Yuan Lu, Broadcom, USA; and Helmut Veith, Vienna U of Techn., Austria
Tree-like counterexamples in model checking
11:30  Sophie Laplante, U Paris XI (Paris-Sud), France; Richard Lassaigne, U Paris VII, France; Frederic Magniez, U Paris XI (Paris-Sud), France; Sylvain Peyronnet, U Paris XI (Paris-Sud), France; and Michel de Rougemont, U Paris II, France
Probabilistic abstraction for model checking: An approach based on property testing
12:00  Thomas Reps, U Wisconsin-Madison, USA; Alexey Loginov, U Wisconsin-Madison, USA; and Mooly Sagiv, Tel Aviv U, Israel
Semantic minimization of 3-valued propositional formulae

12:30-14:00  Lunch

14:00-15:30  Session 3
Chair: Peter O'Hearn

14:00  John C. Reynolds, Carnegie Mellon U, USA
Invited lecture: Separation Logic: A Logic for Shared Mutable Data Structures
15:00  Amal Ahmed, Andrew W. Appel, and Roberto Virga; Princeton U, USA
A stratified semantics of general references embeddable in higher-order logic

15:30-16:00  Refreshments

16:00-17:30  Session 4
Chair: Andy Pitts

16:00  Nadeem A. Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, and Zhaozhong Ni; Yale U, USA
A syntactic approach to foundational proof-carrying code
16:30  Alan Jeffrey, DePaul U, USA and Julian Rathke, U Sussex, UK
A fully abstract may testing semantics for concurrent objects
17:00  Bernhard Reus, U Sussex, UK and Thomas Streicher, U Darmstadt, Germany
Semantics and logic of object calculi

19:00-21:00  City Hall reception (joint with FME, RTA)
Room: City Hall

Tuesday July 23rd

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

09:00-10:30  Session 5
Chair: Furio Honsell

09:00  Jens Palsberg and Tian Zhao, Purdue U, USA
Efficient type inference for record concatenation and subtyping
09:30  Alain Frisch, ENS Paris, France; Giuseppe Castagna, ENS Paris, France; and Véronique Benzaken, U Paris XI (Paris-Sud), France
Semantic subtyping
10:00  Marcelo Fiore, U Cambridge, UK; Roberto Di Cosmo, U Paris VII, France; and Vincent Balat, U Paris VII, France
Remarks on isomorphisms in typed lambda calculi with empty and sum types

10:30-11:00  Refreshments

11:00-12:30  Session 6
Chair: Prakash Panangaden

11:00  Richard Statman, Carnegie Mellon U, USA
On the lambda Y calculus
11:30  Marco Faella, Salvatore La Torre, and Aniello Murano; U Salerno, Italy
Dense real-time games
12:00  Catalin Dima, IMAG Grenoble, France
Computing reachability relations in timed automata

12:30-14:00  Lunch

14:00-15:30  Session 7
Chair: Andrei Voronkov

14:00  Georg Gottlob, Vienna U of Techn., Austria
Invited lecture: Monadic Queries over Tree-Structured Data
15:00  Michael Benedikt, Bell Labs, USA and Leonid Libkin, U Toronto, Canada
Tree extension algebras: Logics, automata, and query languages

15:30-16:00  Refreshments

16:00-17:30  Session 8
Chair: Johann Makowsky

16:00  Markus Frick and Martin Grohe, U Edinburgh, UK
The complexity of first-order and monadic second-order logic revisited
16:30  Jean-Marie Le Bars, U Caen, France
The 0-1 law fails for frame satisfiability of propositional modal logic
17:00  Hajime Ishihara, Japan Advanced Inst. of Science and Techn., Japan; Bakhadyr Khoussainov, U Auckland, New Zealand; and Sasha Rubin, U Auckland, New Zealand
Some results on automatic structures

19:30-22:30  Conference dinner (joint with FME, RTA)
Room: Restaurant Luftkastellet

19:30  Banquet
21:30  Martin Davis, U California-Berkeley, USA
Plenary talk: Alan Turing & the advent of the computer

Wednesday July 24th

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

09:00-10:30  Session 9
Chair: Samson Abramsky

09:00  C.-H. L. Ong, Oxford U, UK
Observational equivalence of 3rd-order idealized Algol is decidable
09:30  Martin Hyland and Andrea Schalk, U Cambridge, UK
Games on graphs and sequantially realizable functionals
10:00  Olivier Laurent, U Paris VII, France
Polarized games

10:30-11:00  Refreshments

11:00-12:30  Session 10
Chair: Andre Scedrov

11:00  Abbas Edalat, Imperial College, UK and Andre Lieutier, Dassault Systemes Provence and LMC/IMAG, France
Domain theory and differential calculus (functions of one variable)
11:30  Alex Simpson, U Edinburgh, UK
Computational adequacy for recursive types in models of intuitionistic set theory
12:00  Daniele Varacca, U Aarhus, Denmark
The powerdomain of indexed valuations

12:30-14:00  Lunch

14:00-15:30  Session 11
Chair: Daniel Leivant

14:00  Stephen A. Cook, U Toronto, Canada
Invited lecture: Complexity Classes, Propositional Proof Systems, and Formal Theories
15:00  William Hesse and Neil Immerman, U Massachusetts, USA
Complete problems for dynamic complexity classes

15:30-16:00  Refreshments

16:00-17:30  Session 12
Chair: Phokion Kolaitis

16:00  Albert Atserias, Techn. U of Catalonia, Spain
Unsatisfiable random formulas are hard to certify
16:30  Michael Soltys, McMaster U, Canada and Stephen A. Cook, U Toronto, Canada
The proof complexity of linear algebra
17:00  Daniel Leivant, Indiana U Bloomington, USA
Calibrating computational feasibility by abstraction rank

17:30-18:10  Session 13: Short Paper Session
Chair: Gordon Plotkin

17:30  Jonathan Ford, U New England, Australia; Ian A. Mason, U New England, Australia; and Natarajan Shankar, SRI International, USA
Short presentation: Lessons learned from formal developments in PVS
17:40  Sylvain Soliman, INRIA Rocquencourt, France
Short presentation: CLP implementation of a phase model checker
17:50  Jens Chr. Godskesen, IT U of Copenhagen, Denmark; Thomas Hildebrandt, IT U of Copenhagen, Denmark; and Vladimiro Sassone, U Sussex, UK
Short presentation: An overview of MR, a calculus of mobile resources
18:00  Claudia Faggian, U Cambridge, UK
Short presentation: Ludics dynamics: Designs and interactive observability

20:00-21:00  LICS Business Meeting

Thursday July 25th

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

09:00-10:30  Session 14
Chair: Franz Baader

09:00  Maurizio Lenzerini, U Rome I (La Sapienza), Italy
Invited tutorial: Description logics: Foundations for class-based knowledge representation
10:00  Martin Otto, U Wales Swansea, UK
Modal and guarded characterisation theorems over finite transition systems

10:30-11:00  Refreshments

11:00-12:30  Session 15
Chair: Doron Peled

11:00  François Laroussinie, Nicolas Markey, and Philippe Schnoebelen; ENS Cachan, France
Temporal logic with forgettable past
11:30  Ian Hodkinson, Imperial College, UK; Frank Wolter, U Leipzig, Germany; and Michael Zakharyaschev, King's College London, UK
Decidable and undecidable fragments of first-order branching temporal logics
12:00  Stephan Kreutzer, Aachen U of Techn., Germany
Expressive equivalence of least and inflationary fixed-point logic

12:30-14:00  Lunch

14:00-15:30  Session 16
Chair: Thomas Streicher

14:00  Josée Desharnais, Laval U, Canada; Vineet Gupta, Stratify Inc., USA; Radha Jagadeesan, Loyola U Chicago, USA; and Prakash Panangaden, McGill U, Canada
The metric analogue of weak bisimulation for probabilistic processes
14:30  Daniel Hirschkoff, ENS Lyon, France; Etienne Lozes, ENS Lyon, France; and Davide Sangiorgi, INRIA Sophia-Antipolis, France
Separability, expressiveness, and decidability in the ambient logic
15:00  Mikkel Nygaard, U Aarhus, Denmark and Glynn Winskel, U Cambridge, UK
Linearity in process languages

15:30-16:00  Refreshments

16:00-17:00  Session 17
Chair: Robert Nieuwenhuis

16:00  Ashish Tiwari, SRI International, USA
Deciding confluence of certain term rewriting systems in polynomial time
16:30  Henrik Björklund and Sergei Vorobyov, Uppsala U, Sweden
Short presentation: Two adversary lower bounds for parity games
16:40  Emmanuel Beffara, ENS Lyon, France and Sergei Vorobyov, Uppsala U, Sweden
Short presentation: Is randomized Gurvich-Karzanov-Khachiyan's algorithm for parity games polynomial?
16:50  Emanuele Covino and Giovanni Pani, U Bari, Italy
Short presentation: Time-space computational complexity of imperative programming languages