LICS 2008 Preliminary Program ==================== Tue Jun 24 ==================== Session 1 (Joint CSF/LICS) 8:30- 9:30 CSF/LICS Joint Invited Talk David Basin Cryptographically Sound Protocol-Model Abstractions 9:30-10:30 Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan (LICS) On the Expressiveness and Complexity of Randomization in Finite State Monitors Henry DeYoung, Deepak Garg and Frank Pfenning (CSF) An Authorization Logic with Explicit Time ----------- 10:30-11:00 Coffee Break ----------- 11:00-12:30 Session 2 (Joint CSF/LICS) Yuri Gurevich and Itay Neeman (CSF) DKAL: Distributed-Knowledge Authorization Language Glenn Bruns and Michael Huth (CSF) Access-Control Policies via Belnap Logic: Effective and Efficient Composition and Analysis Jeffrey Vaughan, Limin Jia, Karl Mazurak and Steve Zdancewic (CSF) Evidence-Based Audit ----------- 12:30- 2:00 Lunch ----------- 2:00- 4:00 Session 3: Logical Frameworks Combining Generic Judgments with Recursive Definitions Andrew Gacek, Dale Miller and Gopalan Nadathur Mechanising the Metatheory of LF Christian Urban, James Cheney and Stefan Berghofer Second-Order and Dependently-Sorted Abstract Syntax Marcelo Fiore Structural Logical Relations Carsten Schürmann and Jeffrey Sarnat ---------- 4:00- 4:30 Coffee Break ---------- 4:30- 5:30 Session 4: Lambda Calculus Types for Hereditary Permutators Makoto Tatsuta Context Matching for Compressed Terms Adrià Gascón, Guillem Godoy and Manfred Schmidt-Schauss ---------- 5:30- 6:30 Session 5: Short Talks (joint CSF/LICS) ---------- 7:00- 9:00 CSF/LICS Joint Reception, Phipps Conservatory ==================== Wed Jun 25 ==================== Session 6 8:30- 9:30 Invited Talk: Dexter Kozen Nonlocal Flow of Control and Kleene Algebra with Tests 9:30-10:30 Algebraic Reasoning A Logic for Algebraic Effects Gordon Plotkin and Matija Pretnar An Algebraic Process Calculus Emmanuel Beffara ---------- 10:30-11:00 Coffee Break ---------- 11:00-12:30 Session 7: Process Calculi On the Expressiveness and Decidability of Higher-Order Process Calculi Ivan Lanese, Jorge A. Perez, Davide Sangiorgi and Alan Schmitt On the Axiomatizability of Impossible Futures: Preorder versus Equivalence Taolue Chen and Wan Fokkink General Structural Operational Semantics through Categorical Logic Sam Staton ---------- 12:30- 2:00 Lunch ---------- 2:00- 4:00 Session 8: Model Checking Parameterization as Abstraction: A Tractable Approach to the Dataflow Analysis of Concurrent Programs Vineet Kahlon Winning Regions of Higher-Order Pushdown Games Arnaud Carayol, Matthew Hague, Antoine Meyer, Luke Ong and Olivier Serre The Ordinal Recursive Complexity of Lossy Channel Systems Pierre Chambart and Philippe Schnoebelen Almost-Sure Model Checking of Infinite Paths in One-Clock Timed Automata Christel Baier, Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye and Marcus Groesser ---------- 4:00- 4:30 Coffee Break ---------- 4:30- 6:00 Session 9: Proof Theory From Axioms to Analytic Rules in Nonclassical Logics Agata Ciabattoni, Nikolaos Galatos and Kazushige Terui Focusing on Binding and Computation Daniel R Licata, Noam Zeilberger and Robert Harper A First-Order Representation of Pure Type Systems using Superdeduction Guillaume Burel ---------- 6:00- 6:30 Award Presentations ---------- 6:30- 7:30 LICS Business Meeting ==================== Thu Jun 26 ==================== Session 10 8:30- 9:30 Invited Talk Martin Grohe The Quest for a Logic Capturing PTIME 9:30-10:30 Computational Complexity On the Asymptotic Nullstellensatz and Polynomial Calculus Proof Complexity Soren Riis On the Computational Complexity of Cut-Reduction Klaus Aehlig and Arnold Beckmann ---------- 10:30-11:00 Coffee Break ---------- 11:00-12:30 Session 11: Constraints Maltsev + Datalog -> Symmetric Datalog Victor Dalmau and Benoit Larose Caterpillar Duality for Constraint Satisfaction Problems Catarina Carvalho, Victor Dalmau and Andrei Krokhin Quantified Constraints and Containment Problems Barnaby Martin, Florent Madelaine and Hubie Chen ---------- 12:30- 2:00 Lunch ---------- 2:00- 4:00 Session 12: Reasoning About Programs Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule Francois Pottier Typed Normal Form Bisimulation for Parametric Polymorphism Soren B. Lassen and Paul Blain Levy Reachability Games and Game Semantics: On Comparing Nondeterministic Programs Andrzej Murawski Weak Topology and Differentiable Operator for Lipschitz Maps Abbas Edalat ---------- 4:00- 4:30 Coffee Break ---------- 4:30- 5:30 Session 13: Probabilistic Systems A Logical Characterization of Individual-Based Models James F. Lynch The Satisfiability Problem for Probabilistic CTL Tomas Brazdil, Jan Kretinsky, Antonin Kucera and Vojtech Forejt ---------- 5:30- 6:30 Session 14: Short Talks ---------- 8:00-10:00 LICS Banquet, History Center ==================== Fri Jun 27 ==================== Session 15 8:30- 9:30 Invited Talk Yiannis Moschovakis The Axiomatic Derivation of Absolute Lower Bounds 9:30-10:30 Finite Model Theory Definable Tree Decompositions Martin Grohe Hypergraph Acyclicity and Extension Preservation Theorems David Duris ---------- 10:30-11:00 Coffee Break ---------- 11:00-12:30 Session 16: Automata Theory From Automatic Structures to Borel Structures Greg Hjorth, Bakhadyr Khoussainov, Antonio Montalbán and Andre Nies Piecewise Testable Tree Languages Mikolaj Bojanczyk, Luc Segoufin and Howard Straubing Collapsible Pushdown Automata and Recursion Schemes Matthew Hague, Andrzej Murawski, Luke Ong and Olivier Serre ---------- 12:30- 1:00 Box Lunch ---------- 1:00- 3:00 Session 17: Linear Logic The Geometry of Interaction of Differential Interaction Nets Marc de Falco Correctness of Multiplicative Additive Proof Structures is NL-Complete Virgile Mogbil and Paulin Jacobé de Naurois Cut Elimination for Monomial MALL Proof Nets Roberto Maieli and Olivier Laurent A Neutral Approach to Proof and Refutation in MALL Olivier Delande and Dale Miller ---------- 3:00 End of Conference ----------