TAPSOFT '95 Preliminary Programme

[Since it is clearly relevant, I am distributing this conference
announcement to types.  -- Philip Wadler, moderator, Types Forum.]


Sixth International Joint Conference on the
Theory and Practice of Software Development


     This abbreviated version is to appear also in Bull. EATCS 55,
     February 1995.  For a copy of the full programme with further
     details see WWW http://www.brics.aau.dk/tapsoft/ - abstracts
     of most of the talks are already available - or contact the 
     TAPSOFT '95 Organisers (tapsoft@brics.aau.dk).


TAPSOFT '95 is the Sixth International Joint Conference on the Theory and
Practice of Software Development.  The TAPSOFT series was started in Berlin
in 1985, on the initiative of H. Ehrig, B. Mahr, and C. Floyd (among
others).  Since then it has been held biennially, in Pisa, Barcelona,
Brighton, and Orsay.

The overall aim of TAPSOFT was formulated as:

     to bring together theoretical computer scientists and software
     engineers (researchers and practitioners) with a view to
     discussing how formal methods can usefully be applied in software

As part of TAPSOFT '95, Ehrig, Mahr and Floyd will review what has been
achieved within the TAPSOFT area during the past decade, and consider
prospects for the future.

TAPSOFT is traditionally divided into three sections:

  *  CAAP: Colloquium on Trees in Algebra and Programming - covering a wide
     range of topics in theoretical computer science

  *  FASE: Colloquium on Formal Approaches in Software Engineering - with
     the emphasis on practical applicability

     H. Ehrig      A Decade of TAPSOFT: Progress and Prospects
     C. Floyd      Theory and Practice of Software Development:
                   Steps in an Unfolding Dance
     M.-C. Gaudel  Testing can be Formal Too
     J. Gougen     Reconciling Social and Technical Aspects of
                   Computer Systems
     D. Kozen      New Results on Set Constraints
     V. Pratt      Rational Mechanics and Natural Mathematics.

In recognition of the importance of support tools for practical use of
formal approaches, TAPSOFT '95 will have two plenary sessions where tools
are demonstrated, as well as opportunities for individual demonstrations.

Facilities will be provided for holding short specialized workshops and
other meetings (e.g., meetings of ESPRIT Basic Research Projects and Working
Groups) in conjunction with TAPSOFT '95.  Please contact the TAPSOFT '95
organisers as soon as possible, if interested, at the address given under
General Information.

The following satellite meetings have already been arranged:

  *  TACAS: Workshop on Tools and Algorithms for the Construction and
     Analysis of Systems
     Friday 19 May - Saturday 20 May
     For details see WWW http://www.brics.aau.dk/tapsoft/tacas/
     or contact Arne Skou (ask@iesd.auc.dk)

  *  TPA: Workshop on Types for Program Analysis
     Friday 26 May (midday) - Saturday 27 May (midday)
     For details see WWW http://www.daimi.aau.dk/~bra8130/TPA/
     or contact Hanne Riis Nielson (hrnielson@daimi.aau.dk)

     Friday 26 May (midday) - Saturday 27 May (midday)
     Members of ESPRIT BR Working Group 6112 (COMPASS) should send abstracts
     of proposed talks to P. D. Mosses (pdmosses@brics.aau.dk) by 15 April.


Friday 19 - Saturday 20 May:

Sunday 21 May, evening:

Monday 22 May, morning:

A Decade of TAPSOFT: Progress and Prospects,
H. Ehrig, B. Mahr (Tech. Univ. Berlin)

CAAP-1:  Trees & Automata              FASE-1:  Types
-------------------------              --------------
First-Order Logic on Finite Trees,     An Imperative Object Calculus,
A. Potthoff (IRISA, Rennes)            M. Abadi, L. Cardelli (Digital SRC,
                                       Palo Alto)
Decidability of Equivalence for
Deterministic Synchronized Tree        A Refinement of Import/Export
Automata, K. Salomaa (Univ. Turku)     Declarations in Modular Logic
                                       Programming and its Semantics,
The Equivalence Problem for            I. Karali, C. Halatsis (Univ. Athens)
Letter-to-Letter Bottom-up
Transducers is Solvable, Y. Andre,     Strictness and Totality Analysis with
F. Bossut (Univ. Lille)                Conjunction, K. L. Solberg (Univ.

Monday 22 May, afternoon:
Theory and Practice of Software Development:  Steps in an Unfolding Dance,
C. Floyd (Univ. Hamburg)

CAAP-2:  Concurrency I                 FASE-2:  Tools
----------------------                 --------------
Internal Mobility and the              Generic Techniques for Source-level
pi-Calculus, D. Sangiorgi (Univ.       Debugging and Dynamic Program
Edinburgh)                             Slicing, F. Tip (CWI, Amsterdam)

Complete Inference Systems for Weak    Reasoning with Executable
Bisimulation Equivalences in the       Specifications, Y. Bertot, R. Fraer
pi-Calculus, H. Lin (Chinese Acad.     (INRIA, Sophia Antipolis)
Sciences, Beijing)
                                       Calculating Software Generators from
Reasoning about Higher Order           Solution Specifications,
Processes, R. Amadio (CRIN-INRIA,      R. B. Kieburtz, F. Bellegarde,
Nancy), M. Dam (SICS, Stockholm)       J. Bell, J. Hook, J. Lewis, D. Oliva,
                                       T. Sheard, L. Walton, T. Zhou (Oregon
Confluence of Processes and Systems    Grad. Inst. Science & Tech.)
of Objects, X. Liu, D. Walker (Univ.

Monday 22 May, evening:

Tuesday 23 May, morning:
New Results on Set Constraints,
D. Kozen (Cornell Univ.)

CAAP-3:  Logic & Specification         FASE-3:  Static Analysis
------------------------------         ------------------------
An Algebraic Approach to Temporal      Comparing Flow-based Binding-time
Logic, B. v. Karger (Chr.-Albrechts    Analyses, J. Palsberg (Univ. Aarhus)
Univ., Kiel)
                                       Can you Trust your Data?  P. Oerbaek
On Behavioural Abstraction and         (Univ. Aarhus)
Behavioural Satisfaction in Higher-
Order Logic, M. Hofmann, D. Sannella   Static and Dynamic Processor
(Univ. Edinburgh)                      Allocation for Higher-Order
                                       Concurrent Languages, H. R. Nielson,
Reasoning about Assumption/Guarantee   F. Nielson (Univ. Aarhus)
Specifications in Linear-Time
Temporal Logic, B. Jonsson,
Y.-K. Tsay (Uppsala Univ.)

Tuesday 23 May, afternoon:
SIGNAL: A Formal Design Environment for Real-Time Systems,
EP-ATR Project (IRISA/INRIA, Rennes)

The META-Frame:  An Environment for Flexible Tool Management,
B. Steffen, T. Margaria, A. Classen (Univ. Passau)

PLATO: A Tool to Assist Programming as Term Rewriting and Theorem Proving,
A. J. Sampaio, A. M. Haeberer, C. T. Prates, C. D. Ururahy, M. F. Frias,
N. C. Albuquerque (PUC, Rio de Janeiro)

The HOL-UNITY Verification System,
F. Andersen, K. D. Petersen, J. S. Pettersson (Tele Danmark Research)

CAAP-4:  Formal Languages              FASE-4:  Case Studies
-------------------------              ---------------------
Fine Hierarchy of Regular              Mechanized Inductive Proof of
omega-Languages, V. Selivanov          Properties of a Simple Code
(Novosibirsk Ped. Univ.)               Optimizer, A. Geser (Univ. Passau)

Computing the Wadge Degree, the        Describing a Signal Analyzer in the
Lifschitz Degree, and the Rabin Index  Process Algebra PMC - A Case Study,
of a Regular Language of Infinite      H. R. Andersen, M. Mendler (Tech.
Words in Polynomial Time, T. Wilke,    Univ. Denmark)
H. Yoo (Chr.-Albrechts Univ., Kiel)
                                       A Gentle Introduction to
Semi-Trace Morphisms and Rational      Specification Engineering using a
Transducers, P.-A. Wacrenier (Univ.    Case Study in Telecommunications,
Bordeaux I)                            S. Kleuker (Univ. Oldenburg)

Nonfinite Axiomatizability of Shuffle
Inequalities, S. L. Bloom (Stevens
Inst. Tech.), Z. Esik (Univ. Szeged)

Wednesday 24 May, morning:
Reconciling Social and Technical Aspects of Computer Systems,
J. Goguen (Oxford Univ.)

CAAP-5:  Concurrency II                FASE-5:  Transformations
-----------------------                ------------------------
On the Category of Petri Net           Precise Interprocedural Dataflow
Computations, V. Sassone (Univ.        Analysis with Applications to
Aarhus)                                Constant Propagation, M. Sagiv,
                                       T. Reps, S. Horwitz (Univ.
High Undecidability of Weak            Wisconsin-Madison)
Bisimilarity for Petri Nets,
P. Jancar (Univ. Ostrava)              Formal Specification and Prototyping
                                       of a Program Specializer, S. Blazy,
Polynomial Algorithms for the          P. Facon (CEDRIC IIE, Evry)
Synthesis of Bounded Nets,
E. Badouel, L. Bernardinello,          Correctness of Recursion-Based
P. Darondeau (IRISA, Rennes)           Automatic Program Transformations,
                                       D. Sands (Univ. Copenhagen)

Wednesday 24 May, afternoon:

Thursday 25 May, morning:
Testing can be Formal too!
M.-C. Gaudel (LRI, Univ. Paris XI)

LOFT: A Tool for Assisting Selection of Test-Sets from Algebraic
Specifications , B. Marre (LRI, Univ. Paris XI)

The SMoLCS Toolset, DISI (Univ. Genova)

The ASF+SDF Meta-environment:  Documentation Tools for Free!,
M. v. d. Brand, E. Visser (Univ. Amsterdam)

Demonstration of the B-Toolkit, I. H. Soerensen (B-Core (UK) Ltd.)

Further tool demonstrations will be given in parallel sessions all week,
  Object Oriented Semantics Directed Compiler Generation - A Prototype,
  L. C. C. Guedes (Univ. Fed. Fluminense), E. H. Haeusler, J. L. Rangel 
  (PUC, Rio de Janeiro)

Thursday 25 May, afternoon:
CAAP-6:  Rewriting Systems             FASE-6:  Concurrency
--------------------------             --------------------
Semi-completeness of Hierarchical and  Reactive System Specification and
Super-hierarchical Combinations of     Refinement, K. Lano (Imperial
Term Rewriting Systems,                College, London)
M. R. K. Krishna Rao (Tata Inst.,
Bombay)                                Measuring Concurrency of Regular
                                       Distributed Computations, C. Bareau
Lazy Narrowing:  Strong Completeness   (IRISA, Rennes), B. Caillaud (Univ.
and Eager Variable Elimination,        Edinburgh), C. Jard (IRISA, Rennes),
S. Okui, A. Middeldorp, T. Ida (Univ.  R. Thoraval (Univ. Nantes)
                                       Non-speculative and Upward Invocation
On the Expressive Power of the         of Continuations in a Parallel
Algebraic Graph Grammars with          Language, L. Moreau (Univ. Liege)
Algebraic Conditions, A. Wagner
(Tech. Univ. Berlin)

The Future of European Spring Conferences on Theory and Practice of Software
Science, chaired by D. Sannella

Thursday 25 May, evening:

Friday 26 May, morning:
Rational Mechanics and Natural Mathematics,
V. Pratt (Stanford Univ.)

CAAP-7:  Semantics                     FASE-7:  Specifications
------------------                     -----------------------
Generated Models and the omega-Rule:   A Model Inference System for Generic
The Nondeterministic Case,             Specification with Application to
M. Walicki, S. Meldal (Univ. Bergen)   Code Sharing, D. Bert, C. Oriat
                                       (LGI-IMAG, Grenoble)
CPO Models for a Class of GSOS
languages, L. Aceto, A. Ingolfsdottir  Relations as Abstract Datatypes:  An
(Aalborg Univ.)                        Institution to Specify Relations
                                       between Algebras, H. Baumeister
Statecharts, Transition Structures     (Max-Planck-Inst., Saarbrucken)
and Transformations, A. Peron (Univ.
Udine)                                 Performance-Oriented Formal
                                       Specifications - the LotoTis
                                       Approach, I. Schieferdecker (GMD
                                       FOKUS, Berlin)

Friday 26 May, afternoon - Saturday 27 May, morning:

CAAP'95 Programme Committee:
     A. Arnold       (France)            J. W. Klop      (Netherlands)
     B. Courcelle    (France)            U. Montanari          (Italy)
     J. Diaz          (Spain)            M. Nielsen   (chair, Denmark)
     V. Diekert     (Germany)            C. Stirling         (Britain)
     H. Ehrig       (Germany)            W. Thomas           (Germany)
     J. Karhumaki   (Finland)            S. Tison             (France)

FASE'95 Programme Committee:
     E. Astesiano   (Italy)           B. Mahr                (Germany)
     D. Basin     (Germany)           F. Orejas                (Spain)
     M.-C. Gaudel  (France)           D. Sannella            (Britain)
     B. Jonsson    (Sweden)           M. Schwartzbach (chair, Denmark)
     P. Klint (Netherlands)           B. Steffen             (Germany)
     B. Lang       (France)           R. Wilhelm             (Germany)

TAPSOFT Steering Committee:  A. Arnold, P. Degano, H. Ehrig,
M.-C. Gaudel, T. Maibaum, U. Montanari, M. Nivat, F. Orejas.

TAPSOFT '95 Organising Committee:  P. D. Mosses (chair),
K. K. Moeller, M. Nielsen, M. I. Schwartzbach.

TAPSOFT '95 is hosted by BRICS (Centre for Basic Research in Computer
Science, Danish National Research Foundation), and sponsored by BRICS,
COMPASS (ESPRIT WG 6112), EATCS (European Association for Theoretical
Computer Science), and by the Dept. of Computer Science and the Faculty
of Science at the University of Aarhus.

General Information
TAPSOFT '95, the Sixth International Joint Conference on the Theory and
Practice of Software Development, will be held at the University of Aarhus,
Denmark.  The TAPSOFT conference itself lasts from Monday 22 May (morning)
to Friday 26 May (midday); TAPSOFT satellite meetings will be held both
before and after, at the same venue.

The Final Programme (available from 15 March 1995) and other information
including abstracts of talks, details of the social programme and
accommodation, together with the registration form can be obtained from:

     Dept. of Computer Science
     University of Aarhus
     Ny Munkegade, Bldg. 540
     DK-8000 Aarhus C, Denmark

     E-mail:  tapsoft@brics.aau.dk
     Telefax:  +45 8942 3255
     WWW: http://www.brics.aau.dk/tapsoft/
     FTP: ftp.brics.aau.dk, get pub/TAPSOFT/README

Aarhus City
Aarhus is the second largest city in Denmark with approximately 265,000
inhabitants, situated on the Eastern coast of the Jutland peninsula.  The
history of Aarhus goes back more than a thousand years and people have lived
in Aarhus ever since the Vikings settled here, where the river flows out
into the bay.

The city has an outstanding location.  The Vikings who selected Aarhus for
their settlement and their home port certainly made a good choice.  Lined
with woods and beaches the city lies in a shielded spot inviting you to
enjoy its many attractions.

Aarhus's thriving cultural atmosphere is to a great extent due to the city's
large student population.  The University of Aarhus, splendidly situated in
a beautifully undulating park, is the largest institution of higher
education in the city, and the second largest university in Denmark with
approximately 16,000 students.

About 40 kilometres west of Aarhus you will find Denmark's most beautiful
lake district around the city of Silkeborg, with interesting museums and an
old steamer boat touring the lakes.  And south-west of Aarhus (about 100
kilometres) is the famous Legoland, an amusement park with models of
landscapes and cities built in toy Lego-bricks.

Aarhus Airport/Tirstrup offers direct flights to and from Copenhagen, Oslo,
Stockholm, Gothenburg, and Brussels.  The airport bus, with service to and
from the central train station, departs from the airport directly after each
arriving flight; it leaves for the airport from the train station 70 minutes
before all departing domestic flights (i.e., to Copenhagen) and 80 minutes
before all departing direct international flights.

Aarhus is served by a train station with an hourly comfortable service to
and from Copenhagen (4 1/2 hours) and several connections daily with Sweden,
Germany, and the rest of Europe.  There is also a harbour conveniently
located in the centre of the city, with ferry and hydrofoil connections with
Copenhagen via Kalundborg.

A freeway links Aarhus directly with Germany and thereby most major European
cities.  Aarhus is a 4 to 5 hour drive from Hamburg.

Within the city, the municipal bus system is a convenient and reliable means
of transportation.  Each TAPSOFT participant will be issued with a bus card
covering local bus travel for the whole week (Monday-Saturday).