[Prev][Next][Index][Thread]
TapSoft'97 : 2nd Call For Paper

To: types@dcs.gla.ac.uk

Subject: TapSoft'97 : 2nd Call For Paper

From: Marc.Tommasi@lifl.fr

Date: Thu, 13 Feb 1997 11:08:02 +0100

DeliveryDate: Thu, 13 Feb 1997 06:15:15 0500

OriginalReceived: from messina.lifl.fr by gordon.lifl.fr, Thu, 13 Feb 1997 12:06:14 +0100

OriginalReceived: by messina.lifl.fr, Thu, 13 Feb 1997 11:08:02 +0100

PPwarning: Illegal Received field on preceding line

PPwarning: Illegal Received field on preceding line
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 1418, 1997  Lille, FRANCE
http://www.lifl.fr/tapsoft97
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
development.
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 CAAPESOPCC.
 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
datastructures, 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 realtime 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
orders"
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
http://www.lifl.fr/tapsoft97/
ftp://ftp.lifl.fr/pub/tapsoft97
AnneCecile.Caron@univlille1.fr
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

REGISTRATION
INVITED LECTURE
Automata on finite trees and partial orders.
W. Thomas, Univ. Kiel
CAAP1 : Rewriting and Automata FASE1 : Specifications

Logicality of Conditional Semantics of Architectural
Rewrite Systems. Connectors.
T. Yamada, LoriaSaenz J.L. Fiadeiro and A. Lopes
J. Avenhaus A. Middeldorp
Simulating ForwardBranching 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
CAAP2 : Automata and Time FASE2 : RealTime 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 HighLevel 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
WaitFree Binary Relations.
E. Goubault
Tuesday 15 april, morning

INVITED LECTURE
Conservative Extensions, Interpretations
between theories and all that.
Tom Maibaum, Imperial College, London
CAAP3 : Termination FASE3 : Types and their Applications

Relative Undecidability in the Reactive Types.
Termination Hierarchy of Single
Rewrite Rules.
A. Geser A. Middeldorp JP. Talpin
E. Ohlebush H. Zantema
Termination Proofs using gpo A TypeBased 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 ProofManager and Graphic Interface for the Larch Prover.
F. Voisin
CAAP4 : Bisimulations and FASE4 : Verification
Picalculus

Modal Characterization of Weak A Comparison of Modular
Bisimulation for Higherorder 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. RealTime 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/OAutomata in
for Giving Coinductive Isabelle/HOLCF.
Characterizations of Observational
Equivalences in Lambdacalculi. O. Mueller T. Nipkow
M. Lenisa
A Labelled Transition Systems
for piepsilonCalculus.
F. Van Breugel
Wednesday 16 april, morning

INVITED LECTURE
Membership Equational Logic.
A. Bouhoula, Nancy and SRIInternational,
J.P. Jouannaud, Univ. Paris XI and SRIInternational, and
J. Meseguer, SRIInternational
CAAP5 : Set Constraints FASE5 : Semantics

Set Operations for Recurrent A Logic of ObjectOriented
term Schematizations. Programs.
A. Amaniss, M. Hermann, M. Abadi, K. Rustan
D. Lugiez M. Leino
Inclusion Constraints over Auxiliary Variables and
Nonempty 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 Webbased 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
semigroups.
P. Caron
CAAP6 : Complexity FASE6 : Static Analysis

Parallel Polynomial Time A Syntactic Theory of Dynamic
Computation and Higher Order Binding.
Recurrence.
D. Leivant J.Y. Marion L. Moreau
On the Complexity of Function A Unified Framework for
Pointer MayAlias Analysis. BindingTime Analysis.
R. Muth S. Debray P. Thiemann
Maximum packing for biconnected A Typed Intermediate Language
outerplanar graphs. for FlowDirected 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
CAAP7 : Unification and Matching FASE7 : Refinement

An algorithm for the solution Action Refinement as an
of tree equations. Implementation Relation.
S. Mantaci D. Micciancio A. Rensink R. Gorrieri
EUnification by Means of Tree SimulationRefinement 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, TUBerlin 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
CAAP8 : Types FASE8 : 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. ArenasSanchez
M. RodriguezArtalejo
Subtyping Constraints for Using LOTOS Patterns to Characterize
Incomplete Objects. Architectural Styles.
V. Bono M. Bugliesi M. Heisel N. L\'evy
M. DezaniCiancaglini
L. Liquori
Partializing Stone Spaces Automating Formal
using SFP domains. SpecificationBased Testing.
F. Alessi P. Baldan M.R. Donat
Furio Honsell
LetPolymorphism and Eager
Type Schemes.
C. Liang