MFCS'93 information booklet, plain text.

[Since it is clearly relevant, I am distributing this conference
announcement to types.  General conference announcements should go to
the Theory-A list.  -- Philip Wadler, moderator, Types Forum.]

The following contains the MFCS'93 information booklet

   l.  19   General information
   l. 553   Registration form
   l. 610   The abstracts of the talks

                        Call for Participation
                      and Preliminary Programme
                     18th International Symposium
             Mathematical Foundations of Computer Science
                           Gdansk, Poland
                    30 August -- 3 September, 1993


The MFCS symposia have been organized in Poland and Czecho-Slovakia
since 1972. Their purpose is to encourage high-quality research in
all branches of Theoretical Computer Science, in particular
   concurrency, lambda calculus, semantics and logics of programs,
   specification, complexity, algorithms, automata theory.

This coming MFCS'93 is organized by the Institute of Computer Science
of the Polish Academy of Sciences.


Basing on comments from more than 230 referees the Programme
Committee has selected 56 papers out of 133 submissions. Twelve
invited speakers complete the Symposium's scientific programme.

All contributions and the invited lectures will be printed in
conference Proceedings. The Proceedings will be published in the
Springer-Verlag LNCS series and will be available during the

Invited Lecturers
   K. R. Apt (Amsterdam)
   A. Arnold (Bordeaux)
   R. M. Burstall (Edinburgh)
   V. Diekert (Stuttgart)
   M. Hennessy (Brighton)
   F. Honsell (Udine)
   R. Milner (Edinburgh)
   A. Pitts (Cambridge)
   V. Pratt (Stanford)
   G. Rozenberg (Leiden)
   A. Salomaa (Turku)
   P. Wadler (Glasgow)

Programme Committee
   J. Adamek (Prague)
   M. Bednarczyk (Gdansk)
   J. A. Bergstra (Amsterdam)
   A. M. Borzyszkowski (Gdansk)
   B. Courcelle (Bordeaux)
   H.-D. Ehrich (Braunschweig)
   I. Havel (Prague)
   G. Huet (Paris)
   N. Jones (Copenhagen)
   E. Moggi (Genova)
   V. Nepomniaschy (Novosibirsk)
   E.-R. Olderog (Oldenburg)
   F. Orejas (Barcelona)
   A. Poigne (St.,Augustin)
   I. Sain (Budapest)
   D. Schmidt (Manhattan, Kansas)
   S. Sokolowski (Gdansk), chair
   M. Wirsing (Munich)


Please address forms and inquiries to the organizers of the

      Institute of Computer Science
      Polish Academy of Sciences
      Jaskowa Dolina 31
      80-252 Gdansk, Poland
      Phone: (+48)(58) 419015 ext. 24,26
      Phone: (+48)(58) 419034 ext. 24,26
      Fax:   (+48)(58) 416912
      E-mail: ssokolow@plearn.bitnet


Sessions A-n and B-n run in parallel.

MONDAY 30 August, morning

Invited Talk 9.50--10.40

Vaughan Pratt
   The second calculus of binary relations

Session A-1 11.10--12.25

Uffe Engberg and Glynn Winskel
   Completeness results for linear logic on Petri nets
A. Fantechi, S. Gnesi, and V. Perticaroli
   An expressive logic for basic process algebra
Regimantas Pliuskevicius
   On saturated calculi for a linear temporal logic

Session B-1 11.10--12.25

Daniele Beauquier and Andreas Podelski
   Rabin tree automata and finite monoids
Karel Culik II and Jarkko Kari
   Image compression using weighted finite automata
Petr Jancar, Frantisek Mraz, and Martin Platek
   A taxonomy of forgetting automata

MONDAY 30 August, afternoon

Invited Talk 14.30--15.20

Phil Wadler
   A taste of linear logic

Session A-2 15.30--16.20

Marcin Benke
   Efficient type reconstruction in the presence of inheritance
Jian Chen and John Staples
   Defining soft sortedness by abstract interpretation

Session B-2 15.30--16.20

Oscar H. Ibarra and Nicholas Tran
   On the communication complexity of parallel computation
Juraj Hromkovic, Jarkko Kari, and Lila Kari
   Some hierarchies for the communication complexity measures of
   cooperating grammar systems

TUESDAY 31 August, morning

Invited Talks 9.00--10.40

Andre Arnold
   Equivalences and preorders on transition systems
Matthew Hennessy
   Symbolic bisimulations

Session A-3 11.10--12.25

Ilaria Castellani
   Observing distribution in processes
David Murphy
   Observing located concurrency
Astrid Kiehn
   Proof systems for cause based equivalences

Session B-3 11.10--12.25

Hans L. Bodlaender and Klaus Jansen
   On the complexity of scheduling incompatible jobs with unit-times
Shiva Chaudhuri, Torben Hagerup, and Rajeev Raman
   Approximate and exact deterministic parallel selection
G. S. Frandsen, P. B. Miltersen, and S. Skyum
   The complexity of finding replicas using equality tests

TUESDAY 31 August, afternoon

Invited Talk 14.30--15.20

Krzysztof R. Apt
   On the unification free Prolog programs

Session A-4 15.30--16.20

Ralf Treinen
   Feature constraints with first-class features
Jilei Yin and Hong Zhu
   Learning decision lists from noisy examples

Session B-4 15.30--16.20

Z. B. Diskin and I. D. Beylin
   Lambda substitution algebras
Don Pigozzi and Antonino Salibra
   A representation theorem for lambda abstraction algebras

Session A-5 16.50--17.40

Christophe Cerin and Antoine Petit
   Speedup of recognizable trace languages
Peter Ruzicka and Juraj Waczulik
   On time-space trade-offs in dynamic graph pebbling

Session B-5 16.50--17.40

Marcello Bonsangue and Joost N. Kok
   Isomorphism between predicate and state transformers
Hermann Puhlmann
   The snack powerdomain for database semantics

WEDNESDAY 1 September, morning

Invited Talks 9.00--10.40

Grzegorz Rozenberg
   An introduction to dynamic labeled 2-structures
Robin Milner
   Concrete action structures

THURSDAY 2 September, morning

Invited Talks 9.00--10.40

Volker Diekert
   Complex and complex-like traces
Arto Salomaa
   Post correspondence problem: Primitivity and interrelations with
   complexity classes

Session A-6 11.10--12.25

V. Arvind, J. Kobler, and M. Mundhenk
   Hausdorff reduction to sparse sets and to sets of high information
Liming Cai and Jianer Chen
   On the amount of nondeterminism and the power of verifying
Bruno Martin
   A uniform universal CREW PRAM

Session B-6 11.10--12.25

Egidio Astesiano, Gianna Reggio, and Elena Zucca
   Stores as homomorphisms and their transformations
J. W. de Bakker, F. van Breugel, and A. de Bruin
   Comparative semantics for linear arrays of communicating processes, a
   study on the UNIX fork and pipe commands
Werner Stephan and Andreas Wolpers
   A calculus for higher order procedures with global variables

THURSDAY 2 September, afternoon

Invited Talk 14.30--15.20

Rod Burstall
   Deliverables: a categorical approach to program development
   in type theory

Session A-7 15.30--16.20

Bernhard Reus and Thomas Streicher
   Verifying properties of module construction in type theory
F. Parisi-Presicce and S. Veglioni
   Heterogeneous unified algebras

Session B-7 15.30--16.20

Bruno Durand
   Global properties of 2D cellular automata: Some complexity results
Jean Neraud
   New algorithms for detecting morphic images of a word

Session A-8 16.50--17.40

Maura Cerioli and Jose Meseguer
   May I borrow your logic?
Nicolas Zabel
   Analytic tableaux for finite and infinite Post logics

Session B-8 16.50--17.40

Jean Berstel and Patrice Seebold
   A characterization of Sturmian morphisms
Philippe Narbel
   The boundary of substitution systems

FRIDAY 3 September, morning

Invited Talks 9.00--10.40

Andrew M. Pitts
   Observable properties of higher order functions that dynamically
   create local names, or: What's  new?
Furio Honsell
   Some results on the full abstraction problem for restricted lambda

Session A-9 11.10--12.25

David Stevens
   Variable substitution with iconic combinators
Roberto M. Amadio
   On the adequacy of PER models
Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro Ugo and Adolfo Piperno
   Filter models for a parallel and non deterministic lambda-calculus

Session B-9 11.10--12.25

Liang Chen
   A model for real-time process algebras
David Scholefield, Hussein Zedan, and He Jifeng
   Real-time refinement: Semantics and application
Bernhard Steffen and Carsten Weise
   Deciding testing equivalence for real-time processes with dense time

FRIDAY 3 September, afternoon

Session A-10 14.30--16.10

Laurent Alonso and Rene Schott
   On the tree inclusion problem
Louis Ibarra and Dana Richards
   Efficient parallel graph algorithms based on open ear decomposition
Egon Wanke
   Paths and cycles in finite periodic graphs
Dorothea Wagner and Frank Wagner
   Between min cut and graph bisection

Session B-10 14.30--16.10

R. J. van Glabbeek
   A complete axiomatization for branching bisimulation congruence of
   finite-state behaviours
Pawel Paczkowski
   Ignoring nonessential interleavings in assertional reasoning on
   concurrent programs
He Jifeng
   Hybrid parallel programming and implementation of synchronised
Vladimiro Sassone, Mogens Nielsen, and Glynn Winskel
   Deterministic behavioural models for concurrency

Session A-11 16.50--17.40

Pietro di Gianantonio
   Real number computability and domain theory.
Michel Parigot and Paul Roziere
   Constant time reductions in lambda-calculus

Session B-11 16.50--17.40

J. F. Costa, A. Sernadas, and C. Sernadas
   Data encapsulation and modularity: Three views of inheritance
E. de Haas and P. van Emde Boas
   Object oriented application flow graphs and their semantics


Borders and customs

A valid passport is required from all foreign guests.  The citizens
of most European states and of the USA need neither entry visas nor
invitations.  The citizens of some countries (eg. Canada, Spain,
Portugal, Greece) would need an entry visa. The citizens of some
other countries (Russia, Byelorussia, Ukraine) would need a formal
invitation from the organizers of MFCS'93.  The holders of
Lithuanian, Latvian or Estonian passports (not the old Soviet ones!)
need neither visa nor invitation.

As the regulations concerning visas keep changing, please find out in
a Polish consulate in your country.  Take into account that
processing your visa application can take a few weeks.

Foreign currencies are easily convertible in Poland in both
directions.  Currently, 1 US $ is worth approximately 17000 Polish
Zlotys but this may change.  It is advisable to declare money at the
border if you bring them in large quantities (eg. 2000 US$) to be
allowed to take them back legally.

Gdansk-Sobieszewo -- the conference site

The city of Gdansk is situated in the North of Poland in the mouth of
Vistula river, 330 km to the North-North-West from Warsaw, the
capital of Poland.  Gdansk is a thousand year old city well known in
both old and recent history.  Amber was traded here in Roman Age.
Later, for hundreds of years Gdansk belonged to Hanza and flourished
on trade with Poland while maintaining its semi-sovereignty.  The
city was shaped by the Germans, Flemish and Danes, even by the
English and Scottish.  Its historical centre is famous for its
brilliant architecture.

The Island of Sobieszewo, a major island in the delta of Vistula
river, used to be a holiday resort for Gdansk citizens.  A lake on
the island is regarded as a "birds paradise".

MFCS'93 is organized in the Baltic Conference Center "ORLE",
Lazurowa 8, 80-680 Gdansk-Sobieszewo.  The distance from the
conference site to the center of Gdansk is 18 km, while the distance
to the white sandy beaches of the Gdansk Bay is 150 m.

Getting there by train

There are convenient railway connections to Gdansk from Warsaw,
Prague, Berlin (via the nearby Gdynia) and from other cities.
Convenient express or intercity trains leave the Warsaw Central
station (Warszawa Centralna) for Gdansk Main (Gdansk Glowny) at
15.57, 16.57 and 17.57. The journey takes three and a half hours and
costs appr. 300000 zl ($18) in first class carriages.

The MFCS participants arriving at Gdansk Main on Sunday, the 29th
August, by any of the three trains mentioned above will be awaited at
the station and put on a special conference bus for Sobieszewo.  We
will extend this option to other trains provided there is enough
interest, so please, fill in the respective information into the
registration form.  There will also be a special transportation from
Sobieszewo to Gdansk Main on Saturday, the 4th September.

On Sundays, buses `112' and `186' depart from their stop at the
Gdansk Main railway station for Sobieszewo every 30 minutes on
average, until 22.26.

Taxi fare from the railway station to the conference site is about
250000zl ($15). To avoid overpaying, please negotiate the price with
the taxi driver before getting into the cab.

Getting there by air

Intercontinental and most international flights to Poland arrive at
Warsaw, 330 km from Gdansk.

Domestic (from Warsaw) and some international flights (eg: Hamburg --
daily, London -- on Saturdays and Mondays) arrive at
Gdansk-Rebiechowo Airport.  If there is enough interest, the special
Symposium's bus transportation will be extended to the airport.

Buses `110' and `L' depart from the airport to the Gdansk-Wrzeszcz
railway station. The ride takes 20 minutes and costs 6000 zl
($0.35).  From there you can take a local train or tramway to Gdansk
Main (Gdansk Glowny) railway station.

Taxi fare from the Airport to the conference site is about 400000 zl

Getting there by car

If you are coming from Warsaw by road no. 7 (E77), turn right in the
village of Przejazdowo, 8 km before the center of Gdansk, continue
over a pontoon bridge to Sobieszewo and further on, some 3 km through
forest.  There, you will come across MFCS posters.

If you are coming from Germany, we suggest the northern route no. 6
(E28) Berlin-Szczecin-Gdynia.  Once in the suburb of Gdynia, turn
right into a dual-carriage way towards Gdansk and Lodz.  This road
avoids the crowded centres of Gdynia, Sopot and most of Gdansk.
Continue for about 20 km and leave at the junction labelled
Gdansk-Centrum.  A 10 km drive will take you to the very centre of
Gdansk; then follow the signs for Warsaw, road no. 7 (E77).  After
some 8 km, in Przejazdowo, turn left and proceed as described above.


On Wednesday, after only two morning talks, a bus excursion is
planned to Malbork and to the old town of Gdansk's, so called Main
Town (Glowne Miasto).

>From the mid-13th until the 15th century, Malbork, or Marienburg, was
the headquarter of the renowned Teutonic Order of monk-knights.  The
Order of the Blessed Virgin Mary's Hospital of the German House, as
was their official denomination, arrived there in the beginning of
the 13th century invited by a Mazovian prince to help in fighting
pagan tribes.  The Teutonic Knigths took over the land and created
their own state which became Poland's most serious problem for the
next couple of centuries.  Their capital, Malbork, was one of the
most inaccessible military strongholds of the time.  The castle is
now reconstructed and homes a museum and several expositions --
amber, old armoury etc.


The weather in the beginning of September is usually mild and sunny
but occasional rains are also possible.  The temperature ranges from
18 to 24 degrees Centigrade at day, and from 8 to 12 degrees
Centigrade at night.  The water temperature in Baltic Sea (the Gulf
of Gdansk) ranges from 15 to 17 degrees Centigrade.


The participants will be lodged in double rooms in the Center.  Rooms
will also be available for single occupancy, at an extra cost.
However, the number of rooms in the Center is limited, and only the
early registration will guarantee a single room reservation.  Those
registering lately should confirm the availability of rooms in
appropriate category before sending any money.

Meals will be served at the conference site, beginning with supper on
Sunday 29 August, and finishing with breakfast on Saturday 4
September.  Please indicate any special dietary requirements on the
registration form.

The registration and information desk will be located at the
conference site.  The registration will start on Sunday, August 29 at


The conference fees in US$ are as follows:

                                   until July 14  after July 14
Pro person in a double room            400            450
Single room                            450            500
Accompanying person in a double room   280            330

The fee includes:
-- 6 day accommodation with full board (3 meals a day) and
   refreshments at coffee breaks from Sunday evening, 29 August, to
   Saturday morning, 4 September, at the Baltic Conference Center;
-- All the social events (welcome drink, excursion, conference banquet,
-- Conference materials, including the Proceedings of the Symposium.

The accompanying persons' fee includes accommodation, board and
social events but no conference materials.

The participants should transfer the equivalent of the fee in their
local currency to the following Bank account:

   Bank Przemyslowo Handlowy w Krakowie
   XIV O/Warszawa
   Account number:  320007-2408
   MFCS'93 <your name>
   Institute of Computer Science
   Polish Academy of Sciences

Make sure that your payment carries your name and quotes "MFCS'93"
as suggested.

A limited number of grants to partially cover conference expenses
will be available.  All the interested are encouraged to apply as
soon as possible.

There is no fee reduction for those who are willing to participate in
a part of the conference only.

In the event of cancellation, the fee will be refunded, except for a
$50 cancellation charge, provided a written request is received by
the conference office by 1st August.  Those whose cancellation
request arrives after 1st August will be sent their Proceedings
volume but no money will be returned.

Please complete and mail the form enclosed together with a copy of
the proof of your payment (by regular mail) to the conference
office.  The reservation will be confirmed after receiving the proof
of payment.

In case of a late registration (after 1st August) we advise to bring
cash rather than to send money via a bank transfer.


Mr/Ms/Dr/Prof ________________________________________

Surname ______________________________________________

Name(s) ______________________________________________

Affiliation __________________________________________

Mailing Address ______________________________________



Phone(s) ___________________ Fax: ____________________

E-mail: ______________________________________________

RATES in US$.  Please indicate the applicable rate by encircling it
on the table, and also writing it in.

                                   until July 14  after July 14
Pro person in a double room            400            450
Single room                            450            500
Accompanying person in a double room   280            330

Total fee: ___________________________________________

Sex: _____ female, _____ male

Name of the preferred roommate (if accommodated in a double room):


Special dietary requirements (vegetarian, etc.) ______


Date of arrival:
  _____ by air to Gdansk; approximate time ___________

  _____ by train to Gdansk; approximate time _________

  _____ by car to Sobieszewo; approximate time _______

Intend to take the conference bus from Gdansk to Sobieszewo:

_____ yes, _____ no.

Date of departure:   _________________________________



Krzysztof R. Apt and Sandro Etalle.
On the unification free Prolog programs.
We provide simple conditions which allow us to conclude that in case
   of several well-known Prolog programs the unification algorithm can
   be replaced by iterated matching. Such a replacement offers a
   possibility of improving the efficiency of program's execution.

Andre Arnold and Dicky A.
Equivalences and preorders on transition systems.
   Two transition systems are logically equivalent if they satisfy the
   same formulas of a given logic. For some of these logics, such as
   Hennessy-Milner's logic, there is an algebraic characterization of
   this equivalence involving particular homomorphisms of transition
   systems. This logical equivalence is associated with a preorder: a
   transition system  A  is less than  A'  if all formulas satisfied by
   A  are satisfied by  A'. For particular logics, this preorder can
   also be algebraically characterized, using homomorphisms and a
   specific notion of inclusion of transition systems.

Rod Burstall.
Proofs in type theory.
A number of groups, including one in Edinburgh, are working on proofs
  in constructive logic using the elegant propositions as types paradigm. Our
  work covers both development of computer checked mathematical theories and
  formal development of software.

Volker Diekert.
Complex and complex-like traces.

A. Ehrenfeucht and Grzegorz Rozenberg.
An introduction to dynamic labeled 2-structures.
   We introduce the theory of dynamic labeled 2-structures. This theory
   forms a framework for investigating (edge-labeled) graphs, where the
   relationships between the nodes may change as a result of actions
   taking place in the nodes. Thus dynamic labeled 2-structures may be
   also seen as models for networks of processes. The lecture presents
   basic properties of dynamic labeled 2-structures and it demonstrates
   useful links with group theory.

Matthew Hennessy.
Symbolic bisimulations.
Most of the traditional verification methods for process description
   languages rely on the fact that the underlying transition systems are
   finite branching. If processes are allowed to send and receive
   messages or values from an infinite data set then this is rarely the
   case. However if we work with "symbolic transition systems" as
   opposed to the usual concrete ones then many of the standard methods
   can still be applied. This talk will survey recent joint work with H.
   Lin and X. Liu on this symbolic approach to message-passing
   processes. This will include a theory of symbolic bisimulations,
   sound and complete proof systems for mesage-passing process calculi
   and a logical characterisation of bisimulation equivalence in terms
   of a first-order modal logic.

Furio Honsell and Marina Lenisa.
Some results on the full abstraction problem for restricted lambda
I will contrast the denotational accounts of the semantics of
   programming languages with other forms of formal description. I will
   speak in favour of the former and its infinite constructions both
   from a foundational and a technical point of view. I will illustrate
   this with some examples. In particular I will discuss some
   non-standard limit constructions. One will show that the notion of
   non erasing function can be adequately captured mathematically. The
   other will be used to show that graspable proofs of operational
   properties of lambda calculi can be obtained form the analysis of the
   fine structure of models.

Alexandru Mateescu and Arto Salomaa.
Post correspondence problem: Primitivity and interrelations with
  complexity classes.
We first introduce the notion of a general primality type, for a
   systematic study of "simple", "primitive" or "prime" solutions of
   the Post Correspondence Problem. We give an exhaustive
   characterization of general primality types. We then introduce
   PCP-related complexity classes, for instance, the time complexity
   classes PCP-P and PCP-NP. While PCP-NP=NP, we can only show that P is
   included in PCP-P.

Robin Milner.
Concrete action structures.
Action structures have been proposed by the author as a general
   model, for concurrent computation. An action structure is a monoidal
   category with two additions: abstractors, which allow the
   parametrization of processes, and reaction, a pre-order upon
   morphisms (i.e. actions) which represents their dynamics. They were
   designed to understand algebraic process calculi, in particular the
   pi-calculus; but the model is wide enough also to supply an
   apparently new algebraic treatment of Petri Nets. The lecture will
   deal with the narrower class of so-called concrete action structures.
   This model allows the pi-calculus (and other process calculi) to be
   seen just as the free extension of a certain elementary action
   structure by adding certain control primitives. This characterization
   offers some hope for a more uniform understanding of process calculi.

Andrew M. Pitts and Ian D. B. Stark.
Observable properties of higher order functions that dynamically
   create local names, or: What's new}?}
This talk is concerned with the problem of reasoning about properties
   of higher order functions involving state. It is motivated by the
   desire to identify what, if any, are the difficulties created purely
   by locality of state, independent of other properties such as
   side-effects, exceptional termination and non-termination due to
   recursion. I consider a simple language (equivalent to a fragment of
   Standard ML) of typed, higher order functions that can dynamically
   create fresh names. Names are created with local scope, can be tested
   for equality and can be passed around by functions, but that is all.
   Nevertheless, the observable behaviour of such functions can be very
   subtle. I will describe a notion of `applicative equivalence' for
   this language incorporating a version of representation independence
   for local names. Applicatively equivalent expressions are
   observationally equivalent, and the converse is true at first order

Vaughan Pratt.
The second calculus of binary relations.
We first review the Peirce-Schroeder calculus of binary relations,
   which equips full linear logic with a nonconstructive noncommutative
   interpretation which elegantly and faithfully models the basic
   elements of sequential control, but which only weakly models Girard's
   axioms. We then reinterpret the same operations over the same domain
   to yield a second calculus of binary relations equipping linear logic
   with a constructive commutative interpretation which elegantly and
   faithfully models the basic elements of concurrent control, and which
   models Girard's axioms as soundly and completely as any
   Chu-construction model.

Phil Wadler.
A taste of linear logic.
Some of the best things in life are free; and some are not. Truth is
   free: having proved a theorem, you may use this proof as many times as
   you wish. Food has a cost: having baked a cake, you may eat it only
   once. In this sense, traditional logic is about truth, while linear
   logic is about food.  This talk will describe connections between
   traditional logic and the type systems used in functional languages
   such as ML and Haskell. It will then go on to describe a type system
   based on linear logic, and its application to improving the
   expressiveness and performance of functional languages.


Laurent Alonso and Rene Schott.
On the tree inclusion problem.
We consider the following problem: Given ordered labeled trees  S
   and  T  can  S  be obtained from  T  by deleting nodes? Deletion of
   the root node  u  of a subtree with children (T_1,...,T_n) means
   replacing the subtree by the trees  T_1,...,T_n . For the tree
   inclusion problem, there can generally be exponentially many ways to
   obtain the included tree.  Recently, P. Kilpelainen and H. Manilla
   gave an algorithm based on dynamic programming requiring  O(|S|.|T|)
   time and space in the worst case and also on the average. We give a
   new algorithm which improves the previous one on the average and
   breaks the  |S|.|T|  barrier.

Roberto M. Amadio.
On the adequacy of PER models.
We consider a fixed point extension of the second order lambda
   calculus equipped with a call by value evaluation mechanism. We
   interpret the language in a partial cartesian closed category of
   "directed complete" partial equivalence relations (pers) over a
   domain theoretic model of a type-free, call-by-value, lambda
   calculus. Our main result is that the notions of syntactic and
   semantic convergence coincide.

V. Arvind, J. Koebler, and M. Mundhenk.
Hausdorff reduction to sparse sets and to sets of high information
We investigate the complexity of sets that have a rich internal
   structure and at the same time are reducible to sets of either low or
   very high information content. Measuring the information content of a
   set by the space-bounded Kolmogorov complexity of its characteristic
   sequence, we show that a set in EXPSPACE is not reducible to a set
   having very high information content unless it reduces to a sparse

Egidio Astesiano, Gianna Reggio, and Elena Zucca.
Stores as homomorphisms and their transformations.
We address the problem of giving a clean and uniform mathematical
   model for handling user defined data types in imperative languages,
   contrary to the ad hoc treatment usual in classical denotational
   semantics. The problem is solved by defining the store as a
   homomorphic mapping of an algebraic structure of left values
   modelling containers into another one of right values modelling
   contents. Consequently store transformations can be defined uniformly
   on the principle that they are minimal variations of the store
   embedding some basic intended effects and compatible with the
   homomorphic structure of the store.

Daniele Beauquier and Andreas Podelski.
Rabin tree automata and finite monoids.
   We incorporate finite monoids into the theory of Rabin
   recognizability of infinite tree languages. We define a free monoid
   of infinite trees and associate with each infinite tree language  L a
   language L^  of infinite words over this monoid. Using this
   correspondence we introduce strong} monoid recognizability of
   infinite tree languages (strengthening the standard notion for
   infinite words) and show that it is equivalent to Rabin
   recognizability. We also show that there exists an infinite tree
   language  L  which is not Rabin recognizable, but its associated
   language  L^  is monoid recognizable (in the standard sense).

Marcin Benke.
Efficient type reconstruction in the presence of inheritance.
The complexity of type reconstruction for simply-typed lambda
   calculus with subtype relation resulting from single inheritance (i.e.
   being a disjoint union of tree-like posets) is analyzed. As a result
   a class of poset including (but not restricted to) trees is defined,
   for which the said problem is solvable in polynomial time.

Jean Berstel and Patrice Seebold.
A characterization of Sturmian morphisms.
A morphism is called Sturmian if it preserves all Sturmian (infinite)
   words. It is called weakly Sturmian if it preserves at least one
   Sturmian word. We prove that a morphism is Sturmian if and only if it
   keeps the word  ba^2ba^2baba^2bab  balanced. As a consequence, weakly
   Sturmian morphisms are Sturmian. An application to infinite words
   associated to irrational numbers is given.

Hans L. Bodlaender and Klaus Jansen.
On the complexity of scheduling incompatible jobs with
We consider scheduling problems in a multiprocessor system with
   incompatibile jobs of unit-time length where two incompatible jobs can
   not be processed on the same machine. Given a deadline  k'  and a
   number of  k machines, the problem is to find a feasible assignment
   of the jobs to the machines. We prove the computational complexity of
   this scheduling problem restricted to different graph classes
   (cographs, bipartite graphs and interval graphs), arbitary and
   constant numbers  k  and  k' .

Marcello Bonsangue and Joost N. Kok.
Isomorphism between predicate and state transformers.
We study the relation between state transformers based on directed
   complete partial orders and predicate transformers. Concepts like
   "predicate", "liveness", "safety" and "predicate transformers"
   are formulated in a topological setting. We treat state transformers
   based on the Hoare, Smyth and Plotkin power domains and consider
   continuous, monotonic and unrestricted functions. We relate the
   transformers by isomorphisms thereby extending and completing earlier
   results and giving a complete picture of all the relationships.

Liming Cai and Jianer Chen.
On the amount of nondeterminism and the power of verifying.
The relationship between nondeterminism and other computational
   resources is studied based on a special interactive-proof system
   model GC(s(n),C) which is a verifier in  C  that can make an extra 
   O(s(n))  amount of nondeterminism. We show that for many functions 
   s(n)  and for many complexity classes  C,  the class GC(s(n),C)  has
   natural complete languages, and that the classes GC(s(n),\Pi_h^0),
   h>=1,  characterize precisely the fixed-parameter intractability of
   NP-hard optimization problems, where  \Pi_h^0  is the class of
   languages accepted by log-time k-alternation ATMs.

Ilaria Castellani.
Observing distribution in processes.
The distributed structure of CCS processes can be made explicit by
   assigning different locations} to their parallel components.  These
   locations then become  part of what is observed of a process.  The
   dynamic approach was developed first, in [BCHK91a], [BCHK91b], as it
   seemed more convenient for defining notions of location equivalence}
   and preorder}.  However, it has the drawback of yielding infinite
   transition system representations.  The static approach, which is
   more intuitive but technically more elaborate, was later developed by
   L. Aceto [Ace91] for nets of automata}, a subset of CCS where
   parallelism is only allowed at the top level.  In this approach each
   net of automata has a finite representation, and one may derive
   notions of equivalence and preorder which coincide with the dynamic
   ones.  The present work generalizes the static treatment of Aceto to
   full CCS.  The result is a distributed semantics which yields finite
   transition systems for all CCS processes with a regular behaviour.

Christophe Cerin and Antoine Petit.
Speedup of recognizable trace languages.
Traces have been defined by A. Mazurkiewicz in order to modelize
   concurrent processes. The decomposition of a trace in foata normal
   form gives the "best" parallel execution of a trace. We define
   naturally the speedup of a trace as the quotient of its sequential
   execution time by its parallel execution time. We generalize this
   definition to trace languages and we prove that this speedup can be
   computed in a modular way for any recognizable trace language.

Maura Cerioli and Jose Meseguer.
May I borrow your logic?
A general and simple construction is presented that allows borrowing
   the components (as well as their associated tools if any) from a logic
   that has them in order to enrich another logic missing such features.
   The relevant structure is transported using maps involving only some
   limited aspect of the two logics in question---for example their
   model theory.

Shiva Chaudhuri, Torben Hagerup, and Rajeev Raman.
Approximate and exact deterministic parallel selection.
   The selection problem is to find the element of prescribed rank  r in
   an ordered set. We study approximate and exact selection on
   deterministic CRCW PRAMs, where approximate selection asks for any
   element whose true rank is close to  r. Our main results are
   work-optimal approximate selection from n-element sets in  
   O((loglog n)^4)  time and work-optimal exact selection from  n-element 
   sets in  O(log n/loglog n)  time.

Jian Chen and John Staples.
Defining soft sortedness by abstract interpretation.
To overcome limitations of conventional sorted languages, soft
   sorting adds sort signatures to an unsorted language without a priori
   restrictions on well-formedness of expressions. Then, the semantics
   defines the significance of the sort syntax. This paper shows how
   soft sortedness can be defined by abstract interpretations, so as to
   characterise semantic properties of softly sorted expressions.

Liang Chen.
A model for real-time process algebras.
We present a general model, Timed Synchronization Trees, for
   real-time systems. Timed synchronization trees are extensions of
   synchronization trees with time. All constructions are continuous
   with respect to a natural CPO. This allows us to interpret a wide
   range of real-time process algebras. As an example, we give a
   denotational semantics for Timed CCS based on timed synchronization

J. F. Costa, A. Sernadas, and C. Sernadas.
Data encapsulation and modularity: Three views of
A rich mechanism of inheritance, including both specialization and
   abstraction, is essential for supporting the envisaged levels of
   software reuse. We adopt the view that an object is a state-machine,
   adapting the notion of reactive system. Then, we develop the notion
   of object morphism in order to explain the basic relationhips between
   objects: is-a and is-part-of.

Karel Culik II and Jarkko Kari.
Image compression using weighted finite automata.
We introduce Weighted Finite Automata (WFA) as a tool to define real
   functions, in particular, greyness functions of grey-tone images.
   Mathematical properties and the definition power of WFA have been
   studied by Culik and Karhumaki. Their generative power is
   incomparable with Barnsley's Iterative Function Systems. Here, we
   give an automatic encoding algorithm that converts an arbitrary
   grey-tone-image (a digitized photograph) into a WFA that can
   regenerate it (with or without information loss). The WFA seems to be
   the first image definition tool with such a relatively simple
   encoding algorithm.

J. W. de Bakker, F. van Breugel, and A. de Bruin.
Comparative semantics for linear arrays of communicating processes, a
  study on the UNIX fork and pipe commands.
Operational (O) and denotational (D) semantic models are designed for
   a language incorporating a version of the UNIX fork and pipe
   commands. Taking a simple while language as starting point, a number
   of programming constructs are added which achieve that a program can
   generate a dynamically evolving (linear) array of processes connected
   by channels.  Over these channels sequences of values (`streams') are
   transmitted. Both O  and  D  are defined as (unique) fixed point of a
   contractive higher ord operator. This allows a smooth proof that  O
   and  D  are equivalent. Additional features are the use of hiatons,
   and of both syntactic and semantic versions of continuations.

E. de Haas and P. van Emde Boas.
Object oriented application flow graphs and their semantics.
In this paper we present a language called OOAFG and its semantics.
   OOAFG intends to express parallelism in the context to object
   identity. We believe that the approach to parallelism we take here is
   a kind of parallelism that is relatively unexplored which connects
   both to the world of Object Oriented Programming, and to the dataflow

Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro and Adolfo Piperno.
Filter models for a parallel and non deterministic
Type assignment systems for the parallel and non deterministic
   lambda-calculus are studied together with a denotational semantics
   which is initially defined constructing a set semimodel via Curry
   types. The type system is then enriched with intersection and union
   types, dually reflecting the disjunctive and conjunctive behaviour of
   the operators; a filter model is built whose local structure is
   compared with a Morris style operational semantics.

Pietro di Gianantonio.
Real number computability and domain theory.
We propose a possible implementation, using lazy functional
   programming, of the exact computation on real numbers. Using domain
   theory we analyze this kind of computation. An interesting connection
   between Scott Topology and the topologies on the real line is stated.
   The main original result in this work is the proof that every
   computable functional on real numbers is continuous w.r.t. the
   compact open topology.

Z. B. Diskin and I. D. Beylin.
Lambda substitution algebras.
In the paper an algebraic metatheory of type-free lambda calculus is
   developed. The present version is based on substitution algebras
   introduced by Feldman enriched with a countable family of unary
   operations of lambda-abstraction and a binary operation of
   application. There are proved representation theorems what provides
   completeness theorems.

Bruno Durand.
Global properties of 2D cellular automata: Some complexity
In this paper, we prove the co-NP-completeness of the following
   decision problem: given a 2-dimensional cellular automaton  A, is A 
   injective when restricted to finite configurations not greater than
   its length. In order to prove this result, we introduce two decision
   problems concerning respectively Turing Machines and tilings that we
   prove NP-complete. We then transform problems concerning tilings into
   problems concerning cellular automata.

Uffe Engberg and Glynn Winskel.
Completeness results for linear logic on Petri nets.
Completeness is shown for several versions of Girard's linear logic
   with respect to Petri nets as the class of models. The strongest
   logic considered is intuitionistic linear logic, with $\otimes$,
   $\mathbin{-\mkern-3mu\raise-.21ex\hbox{$\lhook\mkern-3mu \rhook$}}$,
   $\vphantom{\oplus}\raise-1.15pt\hbox{\rm\&}$, $\oplus$ and the
   exponential ${!}$ ("of course"), and forms of quantification. This
   logic is shown sound and complete with respect to atomic nets (these
   include nets in which every transition leads to a nonempty multiset
   of places). The logic is remarkably expressive, enabling descriptions
   of the kinds of properties one might wish to show of nets; in
   particular, negative properties, asserting the impossibility of an
   assertion, can also be expressed.

A. Fantechi, S. Gnesi, and V. Perticaroli.
An expressive logic for basic process algebra.
In this paper we present a branching time temporal logic for Basic
   Process Algebra. This logic is an enrichment of the branching temporal
   logic CTL with a branching sequential composition operator, named
   chop branching. The logic so obtained is proved to be expressive with
   respect to the bisimulation semantics defined on ${\rm
   BPA}_{{\textstyle \delta},{\textstyle rec}}}$ terms, and is able to
   de scribe context-free properties of systems.

G. S. Frandsen, P. B. Miltersen, and S. Skyum.
The complexity of finding replicas using equality tests.
We prove (for fixed $k$) that at least $\frac{1}{k-1}(^n_2)-O(n)$
   equality tests and no more than $\frac{2}k(^n_2)+O(n)$ equality tests
   are needed in the worst case to determine whether a given set of $n$
   elements contains a subset of $k$ identical elements. The upper bound
   is an improvement by a factor $2$ compared to known results. We give
   tighter bounds for $k=3$.

Juraj Hromkovic, Jarkko Kari, and Lila Kari.
Some hierarchies for the communication complexity measures of
   cooperating grammar systems.
We investigate the descriptional and the computational complexity of
   parallel communicating grammar systems (PCGS). A new descriptional
   complexity measure---the communication structure of the PCGS---is
   introduced and related to the communication complexity (the number of
   communications). Several hierarchies resulting from these complexity
   measures and some relations between the measures are established. The
   results are obtained due to the development of two lower-bound proof
   techniques for PCGS.

Louis Ibarra and Dana Richards.
Efficient parallel graph algorithms based on open ear
We present a new technique called "disjoint decreasing ear paths",
   which is based on a graph's open ear decomposition. We apply this
   technique in CRCW PRAM parallel algorithms for the two vertex
   disjoint s-t paths problem and the maximal path problem in planar
   graphs. These run in  O(log n)  time with  n+m  processors and  
   O(log^2 n)  time with  O(n) processors, respectively, where the 
   graph has n  vertices and  m  edges.

Oscar H. Ibarra and Nicholas Tran.
On the communication complexity of parallel computation.
We argue that the synchronized alternating finite automaton (SAFA) is
   a viable model for studying the communication complexity of parallel
   computation. This motivates our study of the classes of languages
   accepted by SAFA whose messages are bounded in length by a function
   m(n). We establish tight lower bounds on  m(n)  for some types of
   SAFA to accept nonregular languages and give a characterization of NP
   in terms of SAFA.

Petr Jancar, Frantisek Mraz, and Martin Platek.
A taxonomy of forgetting automata.
Forgetting automata are nondeterministic linear bounded automata
   whose rewriting capability is restricted as follows: each cell of the
   tape can only be "erased" (rewritten by a special symbol) or
   completely "deleted".  All classes of languages corresponding to
   various combinations of operations are considered and classified
   according to the Chomsky hierarchy and (some) other relations among
   them are shown.

He Jifeng.
Hybrid parallel programming and implementation of synchronised
An occam program is usually translated into a machine program
   executed in parallel with a set of system processes such as
   communication protocal and scheduler, where the target program
   appears in a form which cannot be modelled in a purely
   communication-based parallel language since concurrent components
   share variables. This paper presents a mathematical treatment for a
   hybrid language equipped with a parallel construct, whose
   sub-processes can communicate with each other via both channels and
   shared variables. We show how it can help in the implementation of
   concurrency and synchronised communication of occam.

A. Kiehn.
Proof systems for cause based equivalences.
Two proof systems for the congruences of causal bisimulation and
   location equivalence of finite CCS are proposed. They generalize the
   known axiomatizations for restriction free processes which are based
   on the two merge operators of ACP. Since the proof systems only
   differ in three equations they provide a simple means of comparison.

Bruno Martin.
A uniform universal CREW PRAM.
The universality of the Parallel Random-Access Machines is usually
   defined by simulating universal Turing machines or Boolean networks.
   We propose in this paper another definition for the universality of
   the Parallel Random-Access Machines based on cellular automata and we
   discuss the advantages and drawbacks of this simulation. We prove
   that there exists a Concurrent-Read Exclusive-Write Parallel
   Random-Access Machine which is capable of simulating any given
   cellular automaton in constant time. We then derive to the definition
   of complexity classes for the parallel Random-Access Machines and for
   the cellular automata.

David Murphy.
Observing located concurrency.
We present a process algebra with an explicit notion of location, and
   give three semantics for it. Two of these semantics are operational,
   giving a standard interleaving and a wholly distributed model for the
   algebra. The third is denotational, and is based on a topology over
   the set of locations.  This topology allows observers to specify
   which locations are to be regarded as distinct. We show that the
   denotational semantics is fully abstract with respect to the
   interleaving semantics if the topology is indiscrete, and that it
   coincides with the fully distributed semantics if it satisfies the
   separation axiom T_1.

Philippe Narbel.
The boundary of substitution systems.
The global limit set has been introduced in a preceding work as a
   generalization of the way of generating infinite words by
   substitution systems, i.e. by iterating a morphism on a finite
   alphabet. We prove here that the boundary set (the "adherence
   set"), that is the set of the compactification points of a
   progressive substitution language is equal to its global limit set
   plus a rational set of words. This allows us to exhibit conditions to
   conclude that the full boundary is explicitly constructible,
   rationally codable and uncountable. The equivalence problem for
   boundaries is also shown decidable whenever the iterated morphism is

Jean Neraud.
New algorithms for detecting morphic images of a word.
We present efficient algorithms for two subcases of the general
   NP-complete problem which consists in matching patterns with
   -- matching an arbitrary one variable regular
      expression with constants,
   -- matching a two variable pattern.

Pawel Paczkowski.
Ignoring nonessential interleavings in assertional reasoning on
   concurrent programs.
In the adopted assertional framework the inductive assertions method
   is applied to a labelled transition system representing a program
   under verification. A reduced representation of concurrent programs
   is considered, where some nonessential interleavings of actions are
   ignored. To isolate such interleavings Mazurkiewicz's trace
   equivalence is exploited. Decidability of verifying that a given
   labelled transition system is a reduced representation of a program
   is investigated.

Michel Parigot and Paul Roziere.
Constant time reductions in lambda-calculus.

F. Parisi-Presicce and S. Veglioni.
Heterogeneous unified algebra.
The framework of Unified Algebras, recently developed for the
   axiomatic specification of ADT, is modified by introducing again the
   notion of sort as a classification mechanism for elements of a type.
   While retaining the idea of sorts as values, Heterogeneous Unified
   Algebras allow the distinction between certain sorts and the
   definition of subsorts by applying operations to them. A
   Specification Logic (which can be extended to an Institution using
   only injective signature morphisms) is defined, and initial algebra
   and free construction are shown to exist.

Don Pigozzi and Antonino Salibra.
A representation theorem for lambda abstraction algebras.
The concept of a lambda abstraction algebra (LAA) is designed to
   algebraize the untyped lambda calculus. The equational axioms of
   LAA's reflect alpha-conversion and Curry's recursive axiomatization
   of substitution in the lambda calculus. Functional LAA's arise from
   lambda models, the natural models of the lambda calculus. Questions of
   the functional representation of various subclasses of LAA's are an
   important part of the theory. The main result of the paper is a
   stronger version of the functional representation theorem for locally
   finite LAA's, the algebraic analogue of the completeness theorem of
   lambda calculus.

Regimantas Pliuskevicius.
On saturated calculi for a linear temporal logic.
A new type of finitary and infinitary sequential calculi (named the
   saturated ones) for a linear temporal logic is introduced. Instead of
   induction-like postulates the saturated calculi contain some
   sequents, indicating the saturation of the derivation process in
   these calculi.

Hermann Puhlmann.
The snack powerdomain for database semantics.
Recently the use of domain theory for a semantics of databases has
   been proposed. To model set-valued structures in this framework, a
   powerdomain construction will be needed. As an appropriate
   construction a modification of the recently introduced snack
   powerdomain is investigated and shown to be a free algebra. Moreover,
   the construction preserves bounded completeness. A slight
   modification of the snack powerdomain yields the scone powerdomain
   which, additionally, is distributive. Both constructions promise to
   bear fruit in the domain theoretic approach to database semantics.

Bernhard Reus and Thomas Streicher.
Verifying properties of module construction in type theory.
This paper presents a comparison between algebraic
   specifications-in-the-large and a type theoretical formulation of
   modular specifications, called deliverables}. It is shown that the
   laws of module algebra can be translated into the deliverables
   approach and can be proved there in the language of type theory. The
   adequacy of the Extended Calculus of Constructions as a possible
   implementation of type theory is discussed and it is explained how
   the reformulation of the laws is influenced by this choice.

Peter Ruzicka and Juraj Waczulik.
On time-space trade-offs in dynamic graph pebbling.
Pebble game on dynamic graphs is studied as an abstract model for the
   incremental computations. We investigate how the time T and/or space S
   is changing according to the number m of insert-edge/delete-edge
   operations on directed acyclic graphs. We present time-space
   trade-off of the form T=\Theta({n^2 \over S+m})  for the standard
   pebble game on permutation graphs of size  n. In the case of the
   minimal space an extreme (superpolynomial) explosion of the time can
   be related to the small (unite) size change in the graph. When the
   space is not minimal a significant (superpolynomial) time increase
   can also be achieved relative to the small (slowly increasing) change
   of the graph size.

Vladimiro Sassone, Mogens Nielsen, and Glynn Winskel.
Deterministic behavioural models for concurrency.
This paper offers three candidates for a deterministic,
   noninterleaving behaviour model, which generalizes Hoare traces to
   the noninterleaving situation. The three models are all proved
   equivalent in the rather strong sense of being equivalent as
   categories. The models are:  deterministic labelled event structures,
   generalized Mazurkiewicz trace languages, and deterministic languages
   of pomsets.

David Scholefield, Hussein Zedan, and He Jifeng.
Real-time refinement: Semantics and application.
A refinement calculus for the development of real-time systems is
   presented. The calculus is based upon a wide-spectrum language called
   TAM (the Temporal Agent Model), within which both functional and
   timing properties can be expressed in either abstract or concrete
   terms. A specification oriented semantics for the language is given.
   Program development is considered as a refinement process i.e. the
   calculation of a structured program from an unstructured
   specification. A calculus of decomposition is defined. An example
   program is developed.

Bernhard Steffen and Carsten Weise.
Deciding testing equivalence for real-time processes with dense
We present a decision algorithm for testing equivalence of real-time
   systems with a dense time domain. Real-time systems are modelled by
   timed graphs, while the decision algorithm uses "mutually refined"
   timer region graphs. The mutual refinement is important for the
   synchronization of the timers of different real-time systems. Key to
   our decision algorithm is the fact that -- despite the dense time
   domain -- testing can be reduced to Pi-bisimulation in very much the
   same way as in the untimed case.

Werner Stephan and Andreas Wolpers.
A calculus for higher order procedures with global variables.
An arithmetically complete axiom system for Algol-like higher order
   procedures with mode depth one is presented. Such procedures may refer
   to an unbounded number of "hidden" program variables by the use of
   procedural parameters. As a solution, we add additional read
   procedures to the program which are used in pre- and postconditions
   to refer to these "hidden" variables.

David Stevens.
Variable substitution with iconic combinators.
An iconic notation for combinators is introduced, and the extensions
   of combinatory logic needed to work with it are developed. It is shown
   how entire sets of combinators can be defined by just two rules: a
   general abstraction rule, and a general reduction rule. These are the
   only rules needed for variable substitution. It is suggested that the
   technique may have advantages for implementing a functional language.

Ralf Treinen.
Feature constraints with first-class features.
Feature Constraint System have been defined elsewhere, providing a
   record like notion for rational trees and extending Colmerauer's
   rational tree constraint system. We extend the feature constraint
   system of [ST92a] to variable features access $x[v]w$, where $v$ is a
   variable ranging over feature symbols. We show that the
   satisfiability problem of conjunctions of atomic constraints is
   NP-complete. Satisfiability of quantifier-free constraints is shown
   to be decidable, while the $\exists^\star\forall^\star\exists^\star$
   fragment of the first order theory is undecidable.

R. J. van Glabbeek.
A complete axiomatization for branching bisimulation congruence of
   finite-state behaviours.
This paper offers a complete inference system for branching
   bisimulation congruence on a basic sublanguage of CCS for
   representing regular processes with silent moves. Moreover, complete
   axiomatizations are provided for the guarded expressions in this
   language, representing the divergence-free processes, and for the
   recursion-free expressions, representing the finite processes.
   Furthermore it is argued that in abstract interleaving semantics (at
   least for finite processes) branching bisimulation congruence is the
   finest reasonable congruence possible. The argument is that for
   closed recursion-free process expressions, in the presence of some
   standard process algebra operations like partially synchronous
   parallel composition and relabelling, branching bisimulation
   congruence is completely axiomatized by the usual axioms for strong
   congruence together with Milner's first  tau-law a tau X = aX.

Dorothea Wagner and Frank Wagner.
Between min cut and graph bisection.
We investigate a class of graph partitioning problems whose two
   extreme representatives are the well-known Min Cut and Graph
   Bisection problems. The former is known to be efficiently solvable by
   flow techniques, the latter to be NP-complete. The results presented
   in this paper are
   -- a monotony result of the type "The
      more balanced the partition we look for has to be, the harder the problem".
   -- a complexity result clarifying the status of a large part of
      intermediate problems in the class.
   Thus we show the existence and partly localize an "efficiency
   border" between the two extremes.

Egon Wanke.
Paths and cycles in finite periodic graphs.
We consider finite periodic graphs}  G^m  defined by nonnegative
   integer vectors  m  and directed graphs  G  whose edges are labeled
   with integer vector-weights.  G^m  has vertex set 
   V \times \{x |\vec{0}\leq x\leq m\} , and an edge from  (u,x)  to  (v,x+z)
   iff  G  has an edge from  u to  v  with vector weight  z. We show that
   path and cycle problems for finite periodic graphs are
   PSPACE-complete under various restrictions, but solvable in
   polynomial time if the vector weights of the edges are bounded.

Jilei Yin and Hong Zhu.
Learning decision lists from noisy examples.
In the paper we solve an open problem raised by Rivest, show that the
   concept class k-Decision lists can be learned, in the sense of
   Valiant, from random examples with classification noise.

Nicolas Zabel.
Analytic tableaux for finite and infinite Post logics.
   We present a tableau-based calculus for the finite and infinite
   valued Post logics, well suited for automated deduction. We define a
   possible world semantics and a prefixed tableau calculus with
   unification on this basis. The world-information is handled by
   solving constraints which express ordering problems. This calculus is
   advantageously compared with other existing ones.