Theoretical Aspects of Computer Software: Third International Symposium, TACS'97, Sendai, Japan, September 23 - 26, 1997, Proceedings (Lecture Notes in Computer Science)

This book constitutes the refereed proceedings of the Third International Symposium on Theoretical Aspects of Computer Software, TACS'97, held in Sendai, Japan, in September 1997. The book presents 20 revised full papers selected from a total of 46 submissions. Also included are seven invited papers by internationally leading scientists. Among the topics addressed are action calculi, polymorphisms, type theory, lambda calculi, refinement, finite transition systems, model checking, process algebras, logical frameworks, higher-order logics, etc. Strong normalisation in higher-order action calculi....Pages 1-19 Extending ML with semi-explicit higher-order polymorphism....Pages 20-46 Optimal representations of polymorphic types with subtyping (Extended abstract)....Pages 47-76 Cyclic lambda calculi....Pages 77-106 Type system for specializing polymorphism....Pages 107-137 On strictness and totality....Pages 138-164 Sound specialization in the presence of computational effects....Pages 165-190 An axiomatic approach to binary logical relations with applications to data refinement....Pages 191-212 Infinitary domain logic for finitary transition systems....Pages 213-232 Some results in the join-calculus....Pages 233-249 Local model checking for value-passing processes (Extended abstract)....Pages 250-266 Data refinement of remote procedures....Pages 267-294 A type-theoretic approach to deadlock-freedom of asynchronous systems....Pages 295-320 Composable semantic models for actor theories....Pages 321-364 Environments, continuation semantics and indexed categories....Pages 365-390 Comparing object encodings....Pages 391-414 System F with width-subtyping and record updating....Pages 415-438 Relational interpretations of recursive types in an operational setting (Summary)....Pages 439-457 Extending a logical framework with a modal connective for validity....Pages 458-490 Using reflection to build efficient and certified decision procedures....Pages 491-514 Sets in types, types in sets....Pages 515-529 Combining Petri nets and PA-processes....Pages 530-546 Symbolic model-checking method based on approximations and binary decision diagrams for real-time systems....Pages 547-561 Types and models for higher-order action calculi....Pages 562-582 Finite-state transducers as regular Böhm trees....Pages 583-603 Secrecy by typing in security protocols....Pages 604-610 ....Pages 611-638 The framework of action calculi [8] is broad enough to accommodate a variety of disciplines of interaction and computation, and yet has unity in its treatment of naming, abstraction, control and composition.