LICS'97 Program

LICS'97 Program


08:30-09:30     Invited Speaker
                (Chair: Andrew Pitts)

                Luca Cardelli (DEC):
                A Theory of Objects.

09:30-10:00     Coffee break

10:00-12:00     Rewriting & Deduction
                (Chair: Claude Kirchner)

                Franz Baader (RWTH Aachen):
                Combination of Compatible Reduction Orderings 
                that are Total on Ground Terms.

                Adel Bouhoula (INRIA Lorraine & CRIN),
                Jean-Pierre Jouannaud (LRI, CNRS&Université de Paris-Sud):
                Automata-Driven Automated Induction.

                Hubert Comon & Florent Jacquemard
                (LRI, CNRS & Université de Paris-Sud):
                Ground Reducibility is EXPTIME-Complete.

                Roberto Di Cosmo (DMI-LIENS, Paris) and
                Delia Kesner (LRI, CNRS & Université de Paris-Sud):
                Strong Normalization of Explicit Substitutions via Cut
                Elimination in Proof Nets.

12:00-13:30     Lunch

13:30-15:30     Linear Logic & Game Semantics
                (Chair: Pat Lincoln)

                Max Kanovich (Russian State Univ. for the Humanities)
                Takayasu Ito (Tohoku University):
                Temporal Linear Logic Specifications for 
                Concurrent Processes.

                Jim Laird (University of Edinburgh):
                Full Abstraction for Functional Languages with Control.

                Patrick Baillot (IML-CNRS Marseille),
                Vincent Danos (Université Paris 7-CNRS),
                Thomas Ehrhard (IML-CNRS Marseille)
                Laurent Regnier (IML-CNRS Marseille):
                Believe it or not, AJM's Games Model is a Model 
                of Classical Linear Logic.

                Dominic J.D. Hughes (PRG, University of Oxford):
                Games and Definability for System F.

15:30-16:00     Coffee break

16:00-17:30     Model Checking
                (Chair: Ken McMillan)

                Henrik Reif Andersen & Henrik Hulgaard
                (Technical University of Denmark):
                Boolean Expression Diagrams.

                Stefan Dziembowski, Marcin Jurdzinski & Igor Walukiewicz
                (Warsaw University):
                How Much Memory is Needed to Win Infinite Games?

                Michael Huth (Kansas State University) &
                Marta Kwiatkowska (University of Birmingham):
                Quantitative Analysis and Model Checking.

18:30-19:30     Invited Speaker
                (Chair: Moshe Vardi)

                Anita Feferman 
                (Biographer, Independent Scholar, Stanford, CA):
                The Saga of Alfred Tarski: From Warszawa to Berkeley


08:30-10:00     Tutorial
                (Chair: David Basin)

                David McAllester (AT & T Labs):
                Methods of Automated Complexity Analysis for 
                Inference Rules.

10:00-10:30     Coffee break

10:30-12:00     Concurrency
                (Chair: Matthew Hennessy)

                Naoki Kobayashi (University of Tokyo):
                A Partially Deadlock-Free Typed Process Calculus.

                Julian Rathke (University of Sussex):
                Unique Fixpoint Induction for Value-Passing Processes.

                Richard Blute (University of Ottawa),
                Josée Desharnais (McGill University, Montreal),
                Abbas Edalat (Imperial College) &
                Prakash Panangaden (BRICS, University of Aarhus):
                Bisimulation for Labelled Markov Processes.

12:00-13:30     Lunch

13:30-15:30     Temporal Logic & Automata
                (Chair: Colin Stirling)

                Eugene Asarin (Inst. for Information Transmission 
                Problems, Moscow),
                Paul Caspi (VERIMAG),
                Oded Maler (VERIMAG):
                A Kleene Theorem for Timed Automata.

                David Janin (LaBRI - ENSERB, Université de Bordeaux I):
                Automata, Tableaus and a Reduction Theorem for 
                Fixpoint Calculi in Arbitrary Complete Lattices.

                P.S. Thiagarajan (BRICS, University of Aarhus) &
                Igor Walukiewicz (Warsaw University):
                An Expressively Complete Linear Time Temporal Logic for
                Mazurkiewicz Traces.

                Dexter Kozen (Cornell University):
                On the Complexity of Reasoning in Kleene Algebra.

15:30-16:00     Coffee break

16:00-18.00     Finite Model Theory
                (Chair: Anuj Dawar)

                Leonid Libkin (Bell Laboratories):
                On the Forms of Locality over Finite Models.

                Martin Grohe (Albert-Ludwigs-Universität Freiburg):
                Large Finite Structures with Few Lk-Types.

                Kousha Etessami (BRICS, University of Aarhus),
                Moshe Y. Vardi (Rice University) &
                Thomas Wilke (Christian-Albrechts-Universität zu Kiel):
                First-Order Logic with Two Variables and 
                Unary Temporal Logic.

                Oliver Matz & Wolfgang Thomas (Universität Kiel):
                The Monadic Quantifier Alternation Hierarchy over 
                Graphs is Infinite.

20:00           Business meeting


08:30-09:30     Invited Speaker
                (Chair: Damian Niwinski)

                Leszek Pacholski (Instytut Informatyki, Wroclaw):
                Set Constraints.

09:30-10:00     Coffee break

10:00-12:00     Semantics & Domain Theory I
                (Chair: Stephen Brookes)

                Peter John Potts, Abbas Edalat & Martin Hötzel Escardo
                (Imperial College, London):
                Semantics of Exact Real Arithmetic.

                Jon G. Riecke (Bell Laboratories) &
                Anders Sandholm (BRICS, University of Aarhus):
                A Relational Account of Call-by-Value Sequentiality.

                Marcelo Fiore, Gordon Plotkin & John Power 
                (University of Edinburgh):
                Complete Cuboidal Sets in Axiomatic Domain Theory.

                Daniele Turi & Gordon Plotkin (University of Edinburgh):
                Towards a Mathematical Operational Semantics.

12:00-13:30     Lunch

13:30-15:30     Decidability & Complexity Theory
                (Chair: Jan Krajicek)

                Sergei Vorobyov (Max-Planck-Institut für Informatik):
                The "Hardest" Natural Decidable Theory.

                Erich Grädel (RWTH Aachen), Martin Otto (RWTH Aachen) &
                Eric Rosen (Technion Haifa):
                Two-Variable Logic with Counting is Decidable.

                Leszek Pacholski (University of Wroclaw),
                Wieslaw Szwast & Lidia Tendera (University of Opole):
                Complexity of Two-Variable Logic with Counting.

                Guo-Qiang Zhang (University of Georgia) &
                William C. Rounds (University of Michigan):
                Complexity of Power Default Reasoning.

15:30-16:00     Coffee break

16:00-17:30     Types and Constraints
                (Chair: Jens Palsberg)

                Nevin Heintze (Bell Laboratories) &
                David McAllester (AT & T Labs):
                On the Cubic Bottleneck in Subtyping and Flow Analysis.

                Fritz Henglein & Jakob Rehof (Copenhagen University):
                The Complexity of Subtype Entailment for Simple Types.

                Witold Charatonik & Andreas Podelski 
                (Max-Planck-Institut für Informatik):
                Set Constraints with Intersection.

19:30           Banquet (The Royal Castle)


08:30-10:00     Tutorial
                (Chair: Claude Kirchner)

                Hubert Comon (LRI, CNRS & Université de Paris-Sud):
                Applications of Tree Automata in Rewriting and 
                Lambda Calculus.

10:00-10:30     Coffee break

10:30-12:00     Semantics & Domain Theory II
                (Chair: Pierre-Louis Curien)

                Martín Hötzel Escardó (Imperial College, London) &
                Thomas Streicher (Technische Hochschule Darmstadt):
                Induction and Recursion on the Partial Real Line via
                Biquotients of Bifree Algebras.

                Martin Hofmann & Thomas Streicher 
                (Technische Hochschule Darmstadt):
                Continuation Models are Universal for 

                Mariangiola Dezani-Ciancaglini (University of Torino)
                Jerzy Tiuryn & Pawel Urzyczyn (University of Warsaw):
                Discrimination by Parallel Observers.

12:00-13:30     Lunch

13:30-15:00     Unification and Higher-Order Logic
                (Chair: Amy Felty)

                Jean Goubault-Larrecq (G.I.E. Dyade)
                Ramified Higher-Order Unification.

                Iliano Cervesato & Frank Pfenning 
                (Carnegie Mellon University):
                Linear Higher-Order Pre-Unification.

                Raymond McDowell & Dale Miller 
                (University of Pennsylvania):
                A Logic for Reasoning with Higher-Order Abstract Syntax.

Leonid Libkin