[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
-
Delivery-Date: Thu, 13 Feb 1997 06:15:15 -0500
-
Original-Received: from messina.lifl.fr by gordon.lifl.fr, Thu, 13 Feb 1997 12:06:14 +0100
-
Original-Received: by messina.lifl.fr, Thu, 13 Feb 1997 11:08:02 +0100
-
PP-warning: Illegal Received field on preceding line
-
PP-warning: 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 14-18, 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 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
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
Anne-Cecile.Caron@univ-lille1.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
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
Pi-calculus
---------------------------------------------------------------------
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
semigroups.
P. Caron
CAAP-6 : Complexity FASE-6 : 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 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