-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- Programme and Call for Participation CSL'97 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 age. 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: http://www.brics.dk/CSL97 =========================================================================== CSL'97 Conference Programme =========================================================================== MONDAY, AUGUST 25 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 Substitutions 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 TUESDAY, AUGUST 26 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 Logics WEDNESDAY, AUGUST 27 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 THURSDAY, AUGUST 28 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 FRIDAY, AUGUST 29 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 Semantics 12:30-14:00 Lunch End of Conference =========================================================================== CSL'97 Tutorials Programme =========================================================================== SATURDAY, AUGUST 23 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 SUNDAY, AUGUST 24 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 Abstract 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 Abstract 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 Abstract 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 calculi. =========================================================================== Further Information =========================================================================== How to Register ================ To get more detailed information on CSL'97, including information on registering, please visit: http://www.brics.dk/CSL97 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 Bureau. All correspondence concerning registration and accommodation (payment, reservation, cancellation, etc.) should be sent to CSL'97 Aarhus Convention Bureau Raadhuset DK-8000 Aarhus C Denmark 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 Bureau. 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. Grants ================== 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 Denmark Inquiries ================== Organisational inquiries about the conference can be sent to: CSL97@brics.dk Local Organization ================== BRICS, Department of Computer Science University of Aarhus Ny Munkegade DK-8000 Aarhus C Denmark Telephone: +45 8942 3360 Telefax: +45 8942 3255 e-mail: csl97@brics.dk http://www.brics.dk/CSL97 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 Berlin. 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.

Accommodation ============= 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 departure. Social Program ============== Get-together: 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 served. Excursion: Wednesday, August 27, 1997 Programme 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 excursion. 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.