TapSoft'97 : 2nd Call For Paper

Please find enclosed the call for participation for TAPSOFT '97.  This call
and other information on TAPSOFT '97 is also accessible by WWW at
http://www.lifl.fr/tapsoft97.  Sincerely apologize if you receive more
than one copy of this message.

Marc Tommasi
Lab. d'Informatique Fondamentale de Lille -- Bat. M3 -- Cite Scientifique
Univ. de Lille 1 -- 59655 Villeneuve d'Ascq CEDEX -- FRANCE

                     TAPSOFT'97 -- CALL FOR PARTICIPATION

                      April 14-18, 1997 -- Lille, FRANCE 


TAPSOFT'97 is the Seventh International Joint Conference on the Theory
and Practice of Software Development. The TAPSOFT series was started
in Berlin in 1985, on the initiative of Hartmut Ehrig and Christiane
Floyd (among others).  Since then it has been held biennially, in
Pisa, Barcelona, Brighton, Orsay and Aarhus. 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

TAPSOFT is traditionally composed of CAAP -- Colloquium on Trees in
Algebra and Programming, and FASE -- Colloquium on Formal Approaches
in Software Engineering.  In recognition of the importance of support
tools for practical use of formal approaches, TAPSOFT'97 will also
have (at least) a session where TOOLS are demonstrated.

The five first editions of CAAP were held in Lille, from 1976 to 1980.
CAAP'97 will be the last one thus it comes back to Lille. In 1998, a
new joint conference, ETAPS (European joint conferences on Theory and
Practice of Software) will be held yearly in Spring. It is the
successor of TAPSOFT and CAAP-ESOP-CC.

----------------------------------- CAAP ------------------------------------ 

Programme Committee:

S. Abramsky (UK)      A. Arnold (France)               G. Ausiello (Italy) 
C. Boehm (Italy)      M. Dauchet (chair, France)       J. Diaz (Spain)
H. Ehrig (Germany)    P. Franchi Zannettacci (France)  J.-P. Jouannaud (France)
H. Kirchner (France)  U. Montanari (Italy)             M. Nielsen (Denmark)
M. Nivat (France)     J.-F. Perrot (France)            J.-C. Raoult (France)  
S. Tison (France)

CAAP cover a wide range of topics in theoretical computer science;
contributions on the following topics are especially welcome:
properties of discrete structures, the theory of formal languages,
syntax and semantics of programming languages, algorithms and
data-structures, logic and formal verification, theoretical problems
arising in software development.

--------------------------------- FASE --------------------------------------

Programme Committee:

E. Astesiano (Italy)          D. Basin (Germany)    M. Bidoit (chair, France)
E. Brinskma (The Netherlands) L. Cardelli (USA)     A. Finkel (France)
J. Fitzgerald (UK)            P.G. Larsen (Denmark) T. Henzinger (USA)
P. Klint (The Netherlands)    P. Mosses (Denmark)   F. Orejas (Spain)
D. Sannella (UK)              B. Steffen (Germany)  M. Wirsing (Germany)  

This colloquium aims at being a forum where different formal
approaches to problems of software specification, development, and
verification are presented, compared, and discussed. Contributions on
the following topics are especially welcome:

-- formal concepts for software development,
-- software development using formal methods,
-- formal approaches for real-time and distributed systems,
-- provably correct software and verification methods,
-- reports on case studies of applications of formal methods,
-- programming languages and type systems,
-- tools and environments supporting formal approaches -- possibly in 
   conjunction with demonstrations.

--------------------------- INVITED SPEAKERS --------------------------------

     E. Astesiano  (Italy)  : "Formalism and Method"
     J.-P. Jouannaud(France): "Membership Equational Logic"
     T. Maibaum (UK)        : "Conservative Extensions, Interpretations 
                                  between theories and all that"
     P. Mosses(Denmark)     : "The Common Framework Initiative for 
                                  Algebraic Specification and Development"
     W. Thomas(Germany)     : "Automata on finite trees and partial 
     F. Vaandrager(NL)      : "A theory of Testing for Times Automata"

-------------------------- CONFERENCE INFORMATION ---------------------------

Additional information, site information, maps, updates, visa, tourist
info, reservation form, accomodation form etc. can be obtained on




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

TAPSOFT'97 Organizing Committee:
A.C. Caron (chair), Y. Andre, F. Bossut, J.L. Coquide, M. Dauchet, 
R. Gilleron, S. Tison, M. Tommasi.

-------------------------- PRELIMINARY PROGRAMME ----------------------------

  Monday 14 april, morning


                         INVITED LECTURE 

              Automata on finite trees and partial orders.

                        W. Thomas, Univ. Kiel 

CAAP-1 : Rewriting and Automata    FASE-1 : Specifications
Logicality of Conditional          Semantics of Architectural 
Rewrite Systems.         	   Connectors.  
T. Yamada,   Loria-Saenz           J.L. Fiadeiro and A. Lopes             
J. Avenhaus  A. Middeldorp 

Simulating Forward-Branching       Protective Interface 
Systems with Constructor Systems.  Specifications.  
B. Salinier  R. Strandh            G. Leavens  J. Wing                  

Reliable Generalized and Context   Specifying Complex and Structured 
Dependent Commutation Relations.   Systems with Evolving Algebras.   
I. Biermann  B. Rozoy 		   W. May                           

Word into Tree Transducers 
with Bounded Difference.
Y. Andre  F. Bossut 

  Monday 14 april, afternoon

                         INVITED LECTURE 
                A theory of Testing for Times Automata.
                   F. Vaandrager, Univ. of Nijmegen 

CAAP-2 : Automata and Time         FASE-2 : Real-Time and distributed systems
Generalized Quantitative           Compositional Specification of     
Temporal Reasoning: 		   Embedded Systems with Statecharts.
An Automata Theoretic Approach.	   
E.A. Emerson  R.J. Trefler         J. Phillips   P. Scholz           

The Railroad Crossing Problem:     Verification of Message Sequence 
Towards Semantics of Timed 	   Charts via Template Matching.    
Algorithms and their Model-	                                    
Checking in High-Level Languages.                                   
D. Beauquier  A. Slissenko 	   V. Levin  D. Peled               

Model Checking through Symbolic    Probabilistic Lossy Channel 
Reachability Graph.		   Systems.                    
J.-M. Ilie  K. Ajami 		   P. Iyer    M. Narasimha     

Optimal Implementation of 
Wait-Free Binary Relations.
E. Goubault 

  Tuesday 15 april, morning

                         INVITED LECTURE 
               Conservative Extensions, Interpretations 
                    between theories and all that.
                 Tom Maibaum, Imperial College, London 

 CAAP-3 : Termination              FASE-3 : Types and their Applications
Relative Undecidability in the     Reactive Types. 
Termination Hierarchy of Single                    
Rewrite Rules.			                   
A. Geser     A. Middeldorp 	   J-P. Talpin    
E. Ohlebush  H. Zantema 

Termination Proofs using gpo       A Type-Based Approach to 
Ordering Constraints.		   Program Security.        
T. Genet     I. Gnaedig 	   D. Volpano   G. Smith    

Automatically Proving              An applicative module calculus. 
Termination Where Simplification                                  
Orderings Fail.			   J. Courant (LIP, Lyon)        
T. Arts      J. Giesl 

Generating Efficient, 
Terminating Logic Programs.
J.C. Martin  A. King 

  Tuesday 15 april, afternoon

  Tools Demonstrations - 1 

Typelab: An environment for modular program development.
 F.W. von Henke, M. Luther, M. Strecker 

TAS and IsaWin: Generic Interfaces for Transformational
Program Development and Theorem Proving.
 Kolyang, Ch. Lueth, T. Meyer, B. Wolff 

Proving System Correctness with KIV.
 W. Reif, G. Schellhorn, K. Stenzel 

A new Proof-Manager and Graphic Interface for the Larch Prover.
 F. Voisin

CAAP-4 : Bi-simulations and        FASE-4 : Verification     
Modal Characterization of Weak     A Comparison of Modular      
Bisimulation for Higher-order 	   Verification Techniques.     
Processes.			   H.R. Andersen J. Staunstrup  
M. Baldamus   J.  Dingel 	   N. Maretti                   

Formats of Ordered SOS Rules       A Compositional Proof of a           
with Silent Actions.		   Real-Time Mutual Exclusion Protocol. 
I. Ulidowski  I. Phillips 	   K.J. Kristoffersen F. Laroussinie    
				   K.G. Larsen        P. Pettersson     
				   Wang Yi                              

The Congruence Candidate Method    Traces of I/O-Automata in  
for Giving Coinductive 		   Isabelle/HOLCF.            
Characterizations of Observational                            
Equivalences in Lambda-calculi.	   O. Mueller    T. Nipkow    
M. Lenisa 

A Labelled Transition Systems 
for pi-epsilon-Calculus.
F. Van Breugel 

  Wednesday 16 april, morning
                         INVITED LECTURE 
                     Membership Equational Logic.  
          A. Bouhoula, Nancy and SRI-International, 
          J.P. Jouannaud, Univ. Paris XI and SRI-International, and 
          J. Meseguer, SRI-International 

CAAP-5 : Set Constraints           FASE-5 : Semantics
Set Operations for Recurrent       A Logic of Object-Oriented 
term Schematizations.		   Programs.                  
A. Amaniss,   M. Hermann, 	   M. Abadi,     K. Rustan    
D. Lugiez 			   M. Leino                   

Inclusion Constraints over         Auxiliary Variables and    
Non-empty Sets of Trees.	   Recursive Procedures.    
M.  Muller,   J. Niehren  	                            
A. Podelski			   T. Schreiber             

Grid Structure and Undecidable     Locality based Linda: programming 
Constraint Theories.		   with explicit localities.         
F. Seynhaeve  M. Tommasi 	   R. De Nicola  G. Ferrari          
R. Treinen 			   R. Pugliese                       

  Wednesday 16 april, afternoon
  Tools Demonstrations - 2 

A Web-based Animator for Object Specifications in a Persistent Environment.
 M. Richters and M. Gogolla 

Publishing Formal Specifications in Z Notation on World Wide Web.
 L. Mikusiak, M. Adamy and T. Seidmann

DOSFOP - A Documentation Tool for the Algebraic Programming Language OPAL.
 K. Didrich, T. Klein

AG: A set of Maple packages for symbolic computing of automata and
 P. Caron 
CAAP-6 : Complexity                FASE-6 : Static Analysis
Parallel Polynomial Time           A Syntactic Theory of Dynamic  
Computation and Higher Order 	   Binding.                       
D. Leivant    J.Y. Marion 	   L. Moreau                      

On the Complexity of Function      A Unified Framework for  
Pointer May-Alias Analysis.	   Binding-Time Analysis.   
R. Muth       S. Debray 	   P. Thiemann              

Maximum packing for biconnected    A Typed Intermediate Language  
outerplanar graphs.		   for Flow-Directed Compilation. 
T. Kovac      A. Lingas 	   J.B. Wells    A. Dimock        
				   R. Muller     F. Turbak        

Synchronization of a line of 
identical processors at a 
given time.
S. La Torre   M. Napoli
M. Parente 

  Thursday 17 april, morning
                         INVITED LECTURE 
                       Formalism and Method.  
         E. Astesiano and G. Reggio, DISI, Universita di Genova 

CAAP-7 : Unification and Matching  FASE-7 : Refinement
An algorithm for the solution      Action Refinement as an   
of tree equations.		   Implementation Relation.  
S. Mantaci    D. Micciancio 	   A. Rensink    R. Gorrieri 

E-Unification by Means of Tree     Simulation-Refinement of             
Tuple Synchronized Grammars.	   Coalgebraic Specifications           
S. Limet      P. Rety 		   with Coinductive Correctness Proofs. 
				   B. Jacobs                            

Linear interpolation for the 
higher order matching problem.
A. Schubert 

  Thursday 17 april, afternoon

                      SPECIAL PANEL DISCUSSION 
       for the last TAPSOFT (and CAAP), before the first ETAPS
                       Invited panelists
           C. Boehm, Univ. Roma, H. Ehrig, TU-Berlin Univ., 
        M. Nivat, Univ Paris VII, Don Sannella, Univ. Edinburgh

            SOCIAL EVENT                       BANQUET

  Friday 18 april, morning

                         INVITED LECTURE 
             The Common Framework Initiative for Algebraic 
                    Specification and Development.
             Peter D. Mosses, BRICS, University of Aarhus 

CAAP-8 : Types                     FASE-8 : Applications of Formal Methods
                                            to Software Engineering
A semantic Framework for           COMPASS: A Comprehensible  
Functional Logic Programming with  Assertion Method.         
Algebraic Polymorphic Types.	   S. Bonnier    T. Heyer    
P. Arenas-Sanchez  
M. Rodriguez-Artalejo 

Subtyping Constraints for          Using LOTOS Patterns to Characterize  
Incomplete Objects.		   Architectural Styles.                 
V. Bono       M. Bugliesi 	   M. Heisel     N. L\'evy               
M. Dezani-Ciancaglini
L. Liquori 

Partializing Stone Spaces          Automating Formal            
using SFP domains.		   Specification-Based Testing. 
F. Alessi     P. Baldan		   M.R. Donat                   
Furio Honsell 

Let-Polymorphism and Eager 
Type Schemes.
C. Liang