Author(s): Marco Bellia, Pierpaolo Degano, Giorgio Levi (auth.), Mariangiola Dezani-Ciancaglini, Ugo Montanari (eds.)
Series: Lecture Notes in Computer Science 137
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 1982
Language: English
Pages: 416
Tags: Logics and Meanings of Programs; Programming Techniques
Applicative communicating processes in first order logic....Pages 1-14
A machine-level semantics for nondeterministic, parallel programs....Pages 15-25
A formalized proof system for total correctness of while programs....Pages 26-36
Automatic program transformation viewed as theorem proving....Pages 37-46
An enlarged definition and complete axiomatization of observational congruence of finite processes....Pages 47-62
Perluette : A compilers producing system using abstract data types....Pages 63-77
A weakest precondition semantics for communicating processes....Pages 78-90
From abstract model to efficient compilation of patterns....Pages 91-104
Computer-based synthesis of logic programs....Pages 105-115
On some syntactic equivalences of program schemas and related transformations....Pages 116-131
Procedures and concurrency: A study in proof....Pages 132-163
Another characterization of weakest preconditions....Pages 164-177
Powerdomains and nondeterministic recursive definitions....Pages 178-193
Optimizing for a multiprocessor: Balancing synchronization costs against parallelism in straight-line code....Pages 194-211
The simple semantics for Coppo-Dezani-Sallé types....Pages 212-226
Proving the correctness of implementations of shared data abstractions....Pages 227-241
Specification of communicating processes and process implementation correctness....Pages 242-256
A system for reasoning within and about algebraic specifications....Pages 257-282
Tuning algebraic specifications by type merging....Pages 283-304
Communicating agents for applicative concurrent programming....Pages 305-322
On effective computations of non-deterministic schemes....Pages 323-336
Specification and verification of concurrent systems in CESAR....Pages 337-351
Proof of separability A verification technique for a class of security kernels....Pages 352-367
A method for program synthesis....Pages 368-380
The use of transformations to implement an algorithm....Pages 381-406
