LICS'98 Program

LICS'98 Program


7:30 - 9:30    RECEPTION


9:00 - 10:00   Invited talk
               Roger Needham (Cambridge University)
               Logic and Over-Simplification
               (Chair: John Mitchell)

10:00 - 10:30  Coffee break

10:30 - 12:30  Session 1: Finite Model Theory I
               (Chair: Martin Otto)

10:30          Fixed-Point Logics on Planar Graphs
               Martin Grohe (Institut fur Mathematische Logik,

10:55          Existential Second-Order Logic over Strings
               Thomas Eiter (University of Giessen),
               Georg Gottlob (Technische Universitat, Wien),
               Yuri Gurevich (University of Michigan)

11:20 - 11:40  Break

11:40          Ordering Finite Variable Types with Generalized Quantifiers
               Anuj Dawar (University of Wales), Lauri Hella
               (University of Helsinki), Anil Seth (The Institute of
               Mathematical Sciences, Madras)

12:05          Convergence Results for Relational Bayesian Networks
               Manfred Jaeger (Max-Planck-Institut fur Informatik,

12:30 - 2:00   Lunch

2:00 - 4:35    Session 2: Verification
               (Chair: Moshe Y. Vardi)

2:00           The Horn Mu-calculus
               Witold Charatonik (Max-Planck-Institut fur Informatik,
               Saarbruecken), David McAllester (AT&T Labs), Damian
               Niwinski (University of Warsaw), Andreas Podelski
               (Max-Planck-Institut fur Informatik, Saarbruecken),
               Igor Walukiewicz (University of Warsaw)

2:25           On Model Checking for Non-Deterministic Infinite State
               E. Allen Emerson, Kedar S. Namjoshi (University of
               Texas at Austin )

2:50           Freedom, Weakness, and Determinism: From Linear-time to
               Orna Kupferman (UC Berkeley), Moshe Y. Vardi (Rice

3:15 - 3:45    Coffee break

3:45           Efficient Representation and Validation of Proofs
               George C. Necula, Peter Lee (CMU)

4:10           Secure Implementation of Channel Abstractions
               Martin Abadi (DEC), Cedric Fournet, 
               Georges Gonthier (INRIA)  

4:35 - 4:55    Break

4:55 - 5:45    Session 3: Logics
               (Chair: Maarten de Rijke)

4:55           The Logical Role of the Four-Valued Bilattice
               Ofer Arieli, Arnon Avron (Tel-Aviv University)

5:20           Completeness of a Relational Calculus for Program Schemes
               Marcelo F. Frias (Catholic University of Rio de
               Janeiro), Roger D. Maddux (Iowa State University)

8:00           Business Meeting


8:30 - 10:00   Tutorial
               Wolfgang Thomas (University of Kiel)
               Monadic logic and automata: Recent developments
               (Chair: Andre Scedrov)

10:00 - 10:30  Coffee break

10:30 - 12:30  Session 4: Concurrency I
               (Chair: Martin Abadi)

10:30          Phase Semantics and Verification of Concurrent
               Constraint Programs
               Francois Fages (ENS), Paul Ruet (McGill University), 
               Sylvain Soliman (ENS)

10:55          A Congruence Theorem for Structured Operational
               Semantics of Higher-Order Languages
               Karen L. Bernstein (DePaul University)

11:20 - 11:40  Break

11:40          Bisimulation in name-passing calculi without matching
               Michele Boreale (Universita "La Sapienza"), Davide
               Sangiorgi (INRIA)

12:05          The Fusion Calculus: Expressiveness and Symmetry in
               Mobile Processes
               Joachim Parrow (Royal Institute of Technology, Sweden),
               Bjorn Victor (Uppsala University)

12:30 - 2:00   Lunch

2:00 - 4:10    Session 5: Category Theory
               (Chair: Eugenio Moggi)

2:00           Type Theory via Exact Categories
               L. Birkedal (CMU), A. Carboni (University of Milan),
               G. Rosolini (University of Genoa), D.S. Scott (CMU)

2:25           Higher Dimensional Multigraphs
               Claudio Hermida, Michael Makkai (McGill University)
               John Power (University of Edinburgh)

2:50 - 3:20    Coffee break

3:20           An Axiomatics for Categories of Transition Systems as
               Peter Johnstone (University of Cambridge), John Power
               (University of Edinburgh), Toru Tsujishita and Hiroshi
               Watanabe (Hokkaido University), James Worrell (Oxford

3:45           A Theory of Recursive Domains with Applications to
               Gian Luca Cattani (University of Aarhus), Marcelo
               Fiore (University of Sussex),  Glynn Winskel
               (University of Aarhus)

4:10 - 4:30    Break

4:30 - 6:00    Invited talk
               Dirk van Dalen (University of Utrecht)
               L.E.J. Brouwer's intuitionism: a revolution in two
               (Chair: Bill Rounds)


8:30 - 10:00   Tutorial
               Maarten de Rijke (University of Amsterdam)
               Process Operations in Extended Dynamic Logics
               (Chair: Edith Hemaspaandra)

10:00 - 10:30  Coffee break

10:30 - 12:30  Session 6: Theorem Proving and Rewriting
               (Chair: Giuseppe Longo)

10:30          Herbrand's theorem, automated reasoning and semantics
               Andrei Voronkov (Uppsala University)

10:55          The Relation Between Second-Order Unification and
               Simultaneous Rigid E-Unification
               Margus Veanes (Max-Planck-Institut fur Informatik)

11:20 - 11:40  Break

11:40          Decision Problems in Ordered Rewriting
               Hubert Comon (CNRS and LSV), Paliath Narendran (SUNY at
               Albany), Robert Nieuwenhuis (Technical University of
               Catalonia), Michael Rusinowitch (INRIA and CRIN)

12:05          A Stability Theorem in Rewriting Theory
               Paul-Andre Mellies (University of Edinburgh)

12:30 - 2:00   Lunch

2:00 - 3:15    Session 7: Linear Logic
               (Chair: Laurent Regnier)

2:00           Light Affine Logic
               Andrea Asperti (University of Bologna)

2:25           Linear Logic With Boxes
               Ian Mackie (Ecole Polytechnique)

2:50           Coinductive Techniques for Operational Equivalence of
               Interaction Nets
               Maribel Fernandez (ENS), Ian Mackie (Ecole Polytechnique)

3:15 - 3:45    Coffee break

3:45 - 4:35    Session 8: Game Semantics
               (Chair: Dale Miller)

3:45           A fully abstract game semantics for general references
               Samson Abramsky, Kohei Honda (University of Edinburgh),
               Guy McCusker (St. John's College, Oxford)

4:10           Recursive Types in Games: Axiomatics and Process
               Marcelo Fiore (University of Sussex), Kohei Honda
               (University of Edinburgh)

4:35 - 4:55    Break

4:55 - 6:10    Session 9: Type Theory
               (Chair: Luke Ong)

4:55           Realizability for Constructive Theory of Functions and
               Classes and its Application to Program Synthesis
               Makoto Tatsuta (Kyoto University)

5:20           Completeness of Type Assignment Systems with
               Intersection, Union, and Type Quantifiers
               Hirofumi Yokouchi (Gunma University)

5:45           Full Abstraction for First-Order Objects with Recursive
               Types and Subtyping
               Ramesh Viswanathan (Bell Laboratories)

7:15           BANQUET (at the Conference Center)


9:00  - 10:00  Invited talk
               Moshe Y. Vardi (Rice University)
               Linear time vs. branching time: a complexity-theoretic
               (Chair: Robert Constable)

10:00 - 10:30  Coffee break

10:30 - 11:20  Session 10: Calculus and Lambda-Calculus
               (Chair: Vaughan Pratt)

10:30          Calculus in coinductive form
               D. Pavlovic (Kestrel Institute), M.H. Escardo
	       (University of Edinburgh) 

10:55          Invertibility in Lambda-Eta
               Enno Folkerts (SAP-AG)

11:20 - 11:40  Break

11:40 - 12:30  Session 11:  Constraints and Complexity
               (Chair: Bengt Jonsson)

11:40          The First-Order Theory of Ordering Constraints over
               Feature Trees
               Martin Mueller, Joachim Niehren (University of
               Saarlandes), Ralf Treinen (University of Paris-South)

12:05          On Proofs About Threshold Circuits and Counting Hierarchies
               Jan Johannsen (UCSD), Chris Pollett (Boston University)

12:30 - 2:00  Lunch

2:00 - 3:15    Session 12: Concurrency II
               (Chair: Tom Henzinger)

2:00           How to Specify and Verify the Long-Run Average Behavior
               of Probabilistic Systems
               Luca de Alfaro (UC Berkeley)

2:25           Compositional Analysis of Expected Delays in Networks of
               Probabilistic I/O Automata
               Eugene W. Stark, Scott A. Smolka (SUNY at Stony Brook)

2:50           A Logical Characterization of Bisimulation for Labeled
               Markov Processes
               Josee Desharnais (McGill University), Abbas Edalat
               (Imperial College), Prakash Panangaden (McGill University)

3:15 - 3:45    Coffee break

3:45 - 5:45    Session 13: Finite Model Theory II
               (Chair: Erich Graedel)

3:45           Embedded Finite Models, Stability Theory and the Impact
               of Order
               John T. Baldwin (University of Illinois at Chicago),
               Michael Benedikt (Bell Laboratories)

4:10           On Counting Logics and Local Properties
               Leonid Libkin (Bell Laboratories)

4:35 - 4:55    Break

4:55           On the Boundedness Problem for Two-Variable First-Order
               Phokion G. Kolaitis (UC Santa Cruz), Martin Otto (RWTH

5:20           Fragments of existential second-order logic without 0-1
               Jean-Marie Le Bars (University of Caen)
               [KLEENE PRIZE]