CSL'97: Programme and Call for Participation


                   Programme and Call for Participation


           The 1997 Annual Conference on Computer Science Logic

                   Aarhus, Denmark,  25-29 August, 1997

             Organized by BRICS, Department of Computer Science,
                          University of Aarhus
             Sponsored by BRICS, the Danish National Research Foundation
                          and the Danish National Research Council


The 1997 Annual Conference on Computer  Science Logic, CSL'97, will be held
at the Computer Science Department, University of  Aarhus, Denmark, 25 - 29
August, 1997, preceded by Tutorials, 23 - 24 August, 1997.

The conference includes invited talks by the following speakers:

           - Samuel R. Buss, San Diego
           - Hubert Comon, Paris
           - Thierry Coquand, Gothenburg
           - Martin Hyland, Cambridge
           - Neil Immerman, Amherst
           - Nils Klarlund, Murray Hill
           - Yiannis N. Moschovakis, Los Angeles
           - Leszek Pacholski, Wroclaw

The tutorials include a three series of lectures on the theme of Games in
Computer Science Logic. The tutorials speakers are:

           - Samson Abramsky, Edinburgh
           - E. Allen Emerson, Austin
           - Wolfgang Thomas, Kiel
           - Igor Walukiewicz, Warsaw

Preliminary proceedings  will  be available at  the conference,   and final
proceedings will be     published in Springer  Lecture   Notes  in Computer
Science, Springer Verlag. Participants will receive copies of both.

Besides   the   scientific program, the  conference   offers  a nice social
programme  including  a conference  dinner   and an excursion  visiting the
Museum of Prehistory at Moesgaard  and the Old  Town of Aarhus. Amongst the
attractions of Moesgaard are  its collections from  the Viking Age, and the
Grauballe man, one of the only complete preserved  bog bodies from the Iron

A limited number of  student grants covering accommodation, conference  fee
including   refreshments,   lunches,   excursion,  conference   dinner  and
conference material, are available.

Information on registering, student grants, travel etc., can be found after
the conference and tutorials programme below or by visiting:


CSL'97 Conference Programme


08:00-09:15  Registration

09:15-09:30  Welcome

09:30-10:30  Neil Immerman (invited speaker):
             Descriptive Complexity and Model Checking

10:30-11:00  Break

11:00-11:30  L. Staiger:
             Disjunctive omega-Words and Monadic Second-Order Arithmetic

11:30-12:00  D. Pardo, A. Rabinovich, B.A. Trakhtenbrot:
             On Synchronous Circuits over Continuous Time

12:00-12:30  A. Arnold, D. Janin:
             A Note on the Satisfiability Problem in Fixpoint Calculi

12:30-14:00  Lunch

14:00-15:00  Samuel R. Buss (invited speaker):
             Resolution, The Pigeonhole Principle and Proof Complexity

15:00-15:30  M. L. Bonet, N. Galesi:
             Linear Lower Bounds and Simulations in Frege Systems with

15:30-16:00  Break

16:00-16:30  T. Coquand, H. Persson:
             A Proof-Theoretical Investigation of Zantema's Problem

16:30-17:00  E. Pezzoli:
             On the Computational Complexity of Type 2 Functionals

17:00-17:30  P. J. Voda:
             A Simple Ordinal Recursive Normalization of Goedel's T

17:45-       EACSL Business Meeting


09:00-10:00  Thierry Coquand (invited speaker):
             Formal Topology and Inductive Definitions

10:00-10:30  M. Hollenberg:
             Equational Axioms of Test Algebra

10:30-11:00  Break

11:00-11:30  T. Brauener, V. de Paiva:
             A Dependency Formulation for Linear Logic

11:30-12:00  C. Faggian:
             Classical Proofs via Basic Logic

12:00-12:30  P. Baillot, V. Danos, T. Ehrhard, L. Regnier:
             Timeless Games

12:30-14:00  Lunch

14:00-15:00  Nils Klarlund (invited speaker):
             Mona & Fido: The Logic/Automaton Connection in Practice

15:00-15:30  O. Kupferman, R.P. Kurshan, M. Yannakakis:
             Existence of Reduction Hierarchies

15:30-16:00  Break

16:00-16:30  M. Grohe:
             Inversion of the L^k-invariants is Hard

16:30-17:00  A. Durand, R. Fagin, B. Loescher:
             Spectra with only Unary Function Symbols

17:00-17:30  F. Olive:
             A Conjunctive Logical Characterization of Nondeterministic
             Linear Time

17:30-18:00  T. Schwentick:
             Padding and the Expressive Power of Existential Second-Order


09:00-10:00  Yiannis N. Moschovakis (invited speaker):
             Concurrent Recursion
10:00-10:30  R. Backofen, P. Clote:
             Evolution as a Computational Engine
10:30-11:00  Break
11:00-11:30  I. Schiering:
             A Hierarchical Approach to Graph Automata and Monadic
             Second-Order Logic over Graphs

11:30-12:00  N. Schweikardt:
             The Monadic Quantifier Alternation Hierarchy over Grids
             and Pictures

12:00-12:30  A. Ayari, D. Basin, A. Podelski:
             Lisa: A Specification Language Based on WS2S

13:30-       Excursion


09:00-10:00  Hubert Comon (invited speaker):
             Higher-Order Matching and Tree Automata
10:00-10:30  F. Kamarredine, R. Bloo, R. Nederpelt:
             An Approximation of Reductional Equivalence
10:30-11:00  Break
11:00-11:30  A. Barber, P. Gardner, M. Hasegawa, G. Plotkin:
             From Action Calculi to Linear Logic
11:30-12:00  P. Ruet, F. Fages:
             Concurrent Constraint Programming and Mixed Non-Commutative
             Linear Logic
12:00-12:30  M. Hofmann:
             A Mixed Modal/Linear Lambda Calculus with Applications to
             Bellantoni-Cook Safe Recursion
12:30-14:00  Lunch
14:00-15:00  Martin Hyland (invited speaker):
             Constructing Categories of Abstract Games
15:00-15:30  J. Power:
             Categories with Algebraic Structure
15:30-16:00  Break
16:00-16:30  S. Abramsky, G. McCusker:
             Call-by-Value Games
16:30-17:00  R. Heckmann, M. Huth:
             A Duality Theory for Quantitative Semantics
17:00-17:30  T. Hartonas, M. Hennessy:
             Full Abstractness for a Functional/Concurrent Language with
             Higher-Order Value-Passing 

19:00-       Conference Dinner


09:00-10:00  Leszek Pacholski (invited speaker):
             Complexity of Type Inference
10:00-10:30  G. Davydov, I. Davydova:
             Applications of Unsatisfiability
10:30-11:00  Break
11:00-11:30  P. A. Bonatti, N. Olivetti:
             A Sequent Calculus for Circumscription
11:30-12:00  J. Hudelmaier:
             Bicomplete Calculi for Intuitionistic Propositional Logic
12:00-12:30  S. Brass, J. Dix, I. Niemelae, T. C. Przymusinski:
             A Comparison of the Static and the Disjunctive Well-founded
12:30-14:00  Lunch

             End of Conference

CSL'97 Tutorials Programme


09:00-09:15  Welcome
09:15-10:45  Samson Abramsky, Univ. of Edinburgh:
             Game Semantics
10:45-11:15  Break
11:15-12:15  Wolfgang Thomas, Univ. of Kiel:
             Determinacy, the Rabin Tree Theorem and its extensions
12:15-14:00  Lunch
14:00-15:00  Wolfgang Thomas:
             Determinacy, the Rabin Tree Theorem and its extensions
15:00-15:30  Break
15:30-17:00  Samson Abramsky:
             Game Semantics


09:15-10:45  E. Allen Emerson, Univ. of Texas at Austin:
             Games, mu-calculus, and program verification
10:45-11:15  Break
11:15-12:15  Igor Walukiewicz, Univ. of Warsaw:
             Determinacy, the Rabin Tree Theorem and its extensions
12:15-14:00  Lunch
14:00-15:00  Igor Walukiewicz:
             Determinacy, the Rabin Tree Theorem and its extensions
15:00-15:30  Break
15:30-17:00  E. Allen Emerson:
             Games, mu-calculus, and program verification

Tutorial Abstracts

Samson Abramsky:
Game Semantics for Programming Languages

  These  lectures  will give   an introduction  to   game semantics and its
applications   to  modelling   programming   languages.  The   mathematical
structure of categories  of games will be described,  and it  will be shown
how  they can be   used to model a  range   of computational features in  a
precise way.

E. Allen Emerson:
Games, mu-calculus, and Program Verification

  Temporal logics are  often used to  verify concurrent programs using such
techniques as model checking. We describe some intimate connections between
such temporal logics, the related fixpoint logic  known as the mu-calculus,
and infinite games.  Applications include improved nonemptiness  algorithms
for  tree automata, mu-calculus  characterizations of winning strategies in
memoryless    games,  and an   automata-theoretic   characterization of the
complexity of model checking in the mu-calculus.

Wolfgang Thomas, Igor Walukiewicz:
Determinacy, the Rabin Tree Theorem and its Extensions

  We present a  self-contained proof of  Rabin's Tree Theorem (decidability
of the monadic  theory  of   two successors).  The  proof  uses  memoryless
determinacy of infinite games. We also show some  extensions of the theorem
to  tree-like infinite  graphs  and  discuss  connections with fixed  point

Further Information

How to Register

To get more   detailed information  on  CSL'97,  including information   on
registering, please visit:


We encourage you to  register via this www page,  but alternatively you may
send   an  email  to  csl97@brics.dk  including your  surface  mail address
requesting a copy of the registration form to be forwarded.

Notice  that the  deadline  for  early  registration  (DKK  2000)  has been
extended to  July 11.  Please also note  that there  is a  reduced  student
registration fee (DKK 600).

Registration Fees

             Particip. paid before July 11:  DKK     2000
             Particip. paid after July 11:   DKK     2500
             Student registration:           DKK      600
             Tutorials, paid before July 11: DKK      300
             Tutorials, paid after July 11:  DKK      400

The registration fees  cover refreshments, lunches, excursion,  banquet and
conference material.

See registration form for  payment. If payment is  made by credit card, the
registration form  must be  signed and mailed   or faxed to  the Convention

All correspondence  concerning  registration  and  accommodation  (payment,
reservation, cancellation, etc.) should be sent to

             Aarhus Convention Bureau
             DK-8000 Aarhus C
             Telephone: +45 8612 1177
             Telefax:   +45 8612 0807
             e-mail:    aarhconv@inet.uni-c.dk

Please give phone and/or telefax numbers on all inquiries to the Convention

Accompanying Persons

Please register accompanying persons on the registration form.  Tickets for
lunches, excursion and conference dinner  may be purchased at the registra-
tion desk.


A limited   number of student  grants to  attend  the Conference and/or the
Tutorials  are available.  The  grants  will cover  local expenses  (accom-
modation at  the nearby Youth  Hostel and conference fee, including lunches
and coffees during the conference, excursion  and conference dinner).  They
will not cover travel expenses.

The deadline for application  is July 1, 1997.  To  apply, you fill  out an
application form available from the above mentioned www page, and return it
with a short   description of  your research   activity  and a  letter   of
recommendation from your supervisor or from the head of the department to

             Prof. Mogens Nielsen, CSL'97
             Department of Computer Science
             University of Aarhus
             Ny Munkegade, Building 540
             DK-8000 Aarhus C


Organisational inquiries about the conference can be sent to:


Local Organization

             BRICS, Department of Computer Science
             University of Aarhus
             Ny Munkegade
             DK-8000 Aarhus C
             Telephone: +45 8942 3360
             Telefax:   +45 8942 3255
             e-mail:    csl97@brics.dk

Organizing Committee

             Mogens Nielsen (chair)
             Gian Luca Cattani
             Uffe Engberg
             Karen K. Moeller

Program Committee

             K. Compton  (Ann Arbor)
             J. Flum (Freiburg)
             F. Honsell (Udine)
             J. W. Klop (Amsterdam)
             V. W. Marek (Lexington)
             M. Nielsen (Aarhus, Vice-chair)
             P. Pudlak (Prague)
             E. Robinson (QMW, London)
             A. Tarlecki (Warsaw),
             W. Thomas (Kiel, Chair),
             I. Walukiewicz (Warsaw).

Travel information

By air
  Aarhus  Airport/Tirstrup  is   connected   with  Copenhagen International
Airport  through  19 daily   departures  on  weekdays,  7-8 departures   on
Saturdays and Sundays.  Flying time  is 35 minutes. Aarhus Airport, located
40 km north   of the city,  offers direct  international  flights to  Oslo,
Stockholm, Gothenburg, London Heathrow and Amsterdam.

Billund  Airport, located 100 km south  of Aarhus, has direct international
flight connections to Amsterdam, Brussels,  Paris, Nice, Frankfurt, London,
Birmingham,   Manchester,  Riga,  Oslo,   Bergen, Stavanger,  Stockholm and

By train/car
  From   Southern  and Central Europe,  the  train/car  connections are via
Hamburg/-Flensburg. Travel time from   Hamburg to Aarhus  is  approximately
five hours.

>From Eastern  European countries train connections to  Aarhus go via Poland
and  Copenhagen. Aarhus has  an hourly service  to and  from Copenhagen and
several daily connections   to  Sweden, Germany   and the rest   of Europe.
Travel time Copenhagen-Aarhus is 3 hrs. 15 min.


Aarhus Convention Bureau has  made  preliminary hotel reservations for  the
CSL'97 participants. Please  use the registration  form to book  rooms. The
hotels have   been divided into  three categories  according to standard or
comfort. The organizers cannot  guarantee accommodation to participants who
do not book in advance.  Payment has to be  made directly to the hotel upon

Social Program


Get-together parties will  be held on Friday,  August 22 and Sunday, August
24,  7:00-10:00 pm at  the conference venue.  Beer and  soft drinks will be


             Wednesday, August 27, 1997

  13:30 Departure from  the conference site  to the Museum of Prehistory at
Moesgaard, a culture-historical  museum  which specializes  in  prehistoric
archaeology and ethnography.

The collections are from the Danish prehistory ranging from the Paleolithic
Age to the end of  the Viking Age.   One  of the  major attractions is  the
Grauballe man  - the only completely preserved  bog body  from the Iron Age
(1st  century  BC).  An  ethnographical  special  exhibition about mountain
people   of the Hindu Kush  is  also on show at  Moesgaard.   On the museum
grounds a replica of  a stave church from  the Viking Age is  being erected
this  summer.  The building  is 9.5 m  long  and almost 5 m  wide  and is a
reconstruction of a church found during excavation  in Hoerning Church near
Randers.  The church is built to the north of the  Hedeby house just behind
the museum. Not since  the Viking Age   has a stave   church been built  in
Denmark. The public is invited to follow the reconstruction.

Weather  permitting,  we will take  a  prehistoric walk through  fields and
woods  passing  reconstructions of  Iron  Age houses,  places  of cult, and
dolmens from the Stone Age.  Refreshments will be served on the beach.

16:00 Buses will return to the centre of Aarhus,  more precisely to The Old
Town, an  open-air museum with  more than 75 half-timbered  houses, rebuilt
along cobbled streets and fitted out with all the workshops and furnishings
of  a Danish market  town, reflecting  life from 1600   down to our  grand-
parents' time.

A  meal  in the  Old Town  restaurant, Simonsen's  Garden,  will finish the

Conference Dinner:

The conference dinner will be held  on the evening  of Thursday, August 28,
starting at 7 pm in the canteen at the conference venue.