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.
Author(s): Robin Milner (auth.), Martín Abadi, Takayasu Ito (eds.)
Series: Lecture Notes in Computer Science 1281
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1997
Language: English
Pages: 648
Tags: Logics and Meanings of Programs; Software Engineering/Programming and Operating Systems; Mathematical Logic and Formal Languages
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
