LICS 2006 Program

Saturday, August 12

Plenary Talk: 9.00-10.00

Formal Verification of Infinite State Systems using Boolean Methods
Randal E. Bryant

Session: Complexity and Decidability 10.30-12.30

Two-Variable Logic on Words with Data
Mikolaj Bojanczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin and Claire David

LTL with the Freeze Quantifier and Register Automata
Stephane Demri and Ranko Lazic

Fixed-Parameter Hierarchies inside PSPACE
Guoqiang Pan and Moshe Vardi

The Boundedness Problem for Monadic Universal First-Order Logic
Martin Otto

Session: Concurrency 2.00-3.30

A Congruence Rule Format for Name-Passing Process Calculi from Mathematical Structural Operational Semantics
Marcelo Fiore and Sam Staton

On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi-Calculus
Catuscia Palamidessi, Vijay Saraswat, Frank D. Valencia and Bjorn Victor

Saturated Semantics for Reactive Systems
Filippo Bonchi, Ugo Montanari and Barbara Koenig

Session: Pushdown Systems 4.00-6.00

On Model-Checking Trees Generated by Higher-Order Recursion Schemes
Luke Ong

Monadic Chain Logic over Iterations and Applications to Pushdown Systems
Dietrich Kuske and Markus Lohrey

An Automata-theoretic Approach for Model Checking Threads for LTL Properties
Vineet Kahlon and Aarti Gupta

On Typability for Rank-2 Intersection Types with Polymorphic Recursion
Tachio Terauchi and Alex Aiken

Sunday, August 13

Invited Talk 9.00-10.00

Adapting Logics
Andreas Blass

Session: Logics of Programs 10.30-12.30

Managing Digital Rights using Linear Logic
Adam Barth and John C. Mitchell

Variables as Resource in Hoare Logics
Matthew Parkinson, Richard Bornat and Cristiano Calcagno

Independence and Concurrent Separation Logic
Jonathan Hayman and Glynn Winskel

Matching Explicit and Modal Reasoning about Programs: A Proof Theoretic Delineation of Dynamic Logic
Daniel Leivant

Session: Proof Theory 2.00-3.30

Context Semantics, Linear Logic and Computational Complexity
Ugo Dal Lago

Obsessional Cliques: A Semantic Characterization of Bounded Time Complexity
Olivier Laurent and Lorenzo Tortora de Falco

A Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives
Alexis Maciel and Toniann Pitassi

Session: Model Theory 4.00-6.00

A Characterisation of First-Order Constraint Satisfaction Problems
Benoit Larose, Cynthia Loten and Claude Tardif

First Order Formulas with Modular Predicates
Laura Chaubard, Jean-Eric Pin and Howard Straubing

On Tractability and Congruence Distributivity
Emil Kiss and Matthew Valeriote

PSPACE Reasoning for Coalgebraic Modal Logic
Lutz Schroder and Dirk Pattinson

Monday, August 14

Invited Talk 9.00-10.00

Avoiding Determinization
Orna Kupferman

Session: Temporal Logics and Automata 10.30-12.30

From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata
Nir Piterman

Memoryful Branching-Time Logic
Orna Kupferman and Moshe Vardi

Faster Solutions of Street and Rabin Games
Nir Piterman and Amir Pnueli

Omega-Regular Expressions with Bounds
Mikolaj Bojanczyk and Thomas Colcombet

Session: Lambda Calculus 2.00-4.00

Head Normal Form Bisimulation for Pairs and the Lambda-Mu Calculus
Soren Lassen

Proof of Strong Normalisation using Domain Theory
Thierry Coquand and Arnaud Spiwack

Boolean Algebras for Lambda Calculus
Giulio Manzonetto and Antonino Salibra

Normalisation is Insensible to Lambda-Term Identity or Difference
Mariangiola Dezani and Makoto Tatsuta

Keynote Session Celebrating Birth Centennial of Kurt Goedel 4.30-6.00

Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Goedel's Impact on Logic, Mathematics, and Computer Science
John Dawson

The Future of Proof
Dana Scott

Tuesday, August 15

Invited Talk 9.00-10.00

Provable Implementations of Security Protocols
Andy Gordon

Session: Timed and Stochastic Systems 10.30-12.30

Stochastic Games with Branching-Time Winning Objectives
Tomas Brazdil, Vaclav Brozek, Vojtech Forejt and Antonin Kucera

Average Time Games
Marcin Jurdzinski and Ashutosh Trivedi

Coinductive Proof Principles for Stochastic Processes
Dexter Kozen

Control in o-minimal Hybrid Systems
Patricia Bouyer, Thomas Brihaye and Fabrice Chevalier

Session: Verification 2.00-3.30

An Abstraction-Refinement Framework for Multi-Agent Systems
Thomas Ball and Orna Kupferman

Temporal Logics and Model Checking for Fairly Correct Systems
Daniele Varacca and Hagen Voelzer

3-Valued Abstraction: More Precision at Less Cost
Sharon Shoham and Orna Grumberg

Session: Approximations 4.00-5.00

Approximation Schemes for First-Order Definable Optimization Problems
Anuj Dawar, Martin Grohe, Stephan Kreutzer and Nicole Schweikardt

Approximate Satisfiability and Equivalence
Eldar Fischer, Frederic Magniez and Michel de Rougemont

Session: Short Presentations 5.00-6.00

A Polynomial-time Algorithm for Uniqueness of Normal Forms of Linear Shallow Term Rewrite Systems
Julian Zinn and Rakesh Verma

Non-Closure Results for First-Order Spectra
Aaron Hunter

A Dolev-Yao-based Definition of Abuse-free Protocols
Detlef Kaehler, Ralf Kuesters and Thomas Wilke

An Abstract Completion Procedure for Cut Elimination in Deduction Modulo
Guillaume Burel and Claude Kirchner

Interactive Correctness Criterion for Multiplicative-Additive Proof-Nets
Roberto Maieli and Paul Ruet

A Logical Look at Agents: Problem-Solving on the Semantic Web
Leona F. Fass

Nominalization in Intensional Type Theory
Joergen Villadsen

Grounding for Model Expansion in k-Guarded Formulas
Murray Patterson, Yongmei Liu, Eugenia Ternovska and Arvind Gupta