Type and Effect Systems

by Amtoft, Torben; Nielson, Flemming; Nielson, Hanne Riis

• ISBN13: 9781860941542
• ISBN10: 1860941540
• Format: Hardcover
• Copyright: 1999-06-01
• Publisher: Imperial College Pr

Summary

Concurrent and distributed processes occur everywhere: in embedded systems, in information networks and databases, and in the form of applets roaming around on the World-Wide-Web. This book presents and develops state-of-the-art validation techniques for detecting safety violations; the focus is on the correctness of techniques that suffice for fully automatic validation of key components of such systems. It builds on and extends the notion of types, popular in many sequential programming languages as a technique for catching certain kinds of errors already at program development time, by incorporating behaviours (or structured effects) that are able to track the information flow in the presence of procedures, channel based communication, and the dynamic creation of network topologies. The technical development is performed for a language based on Concurrent ML.

Table of Contents

Preface	xi
Introduction	1	(42)
Basic Concepts	1	(3)
Polymorphism	4	(9)
An Inference System	5	(2)
An Inference Algorithm	7	(3)
Implicit Treatments of Side Effects	10	(3)
An Inference System for Effects	13	(9)
Effects Controlling Polymorphism	15	(1)
Regions	15	(3)
Behaviours	18	(2)
Subeffecting	20	(2)
An Inference Algorithm for Effects	22	(6)
Effect Constraints	22	(2)
Solving Effect Constraints	24	(1)
Downwards Closure for Polymorphism	25	(3)
Shape Conformant Subtyping with Effects	28	(8)
Inference Systems for Atomic Subtyping	29	(3)
Algorithmic Techniques for Atomic Subtyping	32	(2)
Integrating Shape Conformant Subtyping	34	(2)
Overview of the Development	36	(7)
The Main Ideas	36	(2)
A Prototype Implementation	38	(1)
Benchmarks	39	(1)
A Reader's Guide to the Book	40	(3)
The Type and Effect System	43	(34)
The Source Language	43	(5)
Concurrent Programming	45	(3)
Basic Notions	48	(4)
Regions	48	(1)
Behaviours	49	(1)
Types	49	(1)
Constraints	50	(1)
Miscellaneous	51	(1)
Shape Conformant Subtyping	52	(2)
The Ordering on Behaviours	53	(1)
The Ordering on Types	53	(1)
The Type Inference System	54	(5)
The Rule for Generalisation	59	(5)
Backwards Closure	60	(1)
The Arrow Relation	61	(2)
Well-formed Type Schemes	63	(1)
Pragmatics	64	(3)
Basic Results	67	(5)
Trace Inclusion	70	(1)
Normalisation of Inference Trees	71	(1)
Conservative Extension of Hindley-Milner	72	(5)
The Semantics	77	(22)
The Sequential Semantics	78	(3)
The Concurrent Semantics	81	(1)
Reasoning about Inference Trees	82	(4)
Sequential Soundness	86	(4)
Erroneous Programs cannot be Typed	90	(2)
Concurrent Soundness	92	(7)
The Inference Algorithm	99	(22)
Algorithm W'	101	(3)
Algorithm F	104	(6)
Termination and Soundness	109	(1)
Algorithm R	110	(9)
Termination and Soundness	116	(1)
Confluence Properties	117	(2)
Syntactic Soundness of Algorithm W	119	(2)
The Relation to Hindley-Milner Typing	120	(1)
The Inference Algorithm: Completeness	121	(20)
The Completeness Result for Programs	121	(3)
Applicability of the Completeness Result	123	(1)
The Relation to Hindley-Milner Typing	123	(1)
Completeness of Algorithm F	124	(1)
Completeness of Algorithm R	125	(1)
Lazy Instance for Type Schemes	126	(2)
The Completeness Result for Expressions	128	(13)
The Proof: Lifting from W to W	129	(1)
The Proof: The Case for Type Schemes	130	(4)
The Proof: The Case for Types	134	(7)
Post-processing the Analysis	141	(24)
Solving Region Constraints	142	(1)
A Catalogue of Behaviour Transformations	143	(4)
Simplification	144	(1)
Hiding	145	(1)
Unfolding	145	(1)
Collapsing	146	(1)
The Notion of Bisimulation	147	(4)
Correctness of the Transformations	151	(6)
Simplification	152	(1)
Hiding	153	(1)
Unfolding	154	(2)
Collapsing	156	(1)
A Subject Reduction Property	157	(7)
Semantic Soundness of a Post-processing W	164	(1)
A Case Study	165	(12)
The Production Cell	166	(4)
Safety Conditions for the Table	167	(1)
An Implementation of the Table	167	(2)
The Behaviour of the Table	169	(1)
Validating the Safety Conditions	170	(4)
Vertical Bounds for the Table	171	(1)
Horizontal Bounds for the Table	172	(1)
No Collisions on the Table	173	(1)
Discussion	174	(3)
A Proofs of Results in Chapter 2	177	(18)
A.1 Proofs of Results in Section 2.5	177	(1)
A.2 Proofs of Results in Section 2.7	178	(5)
A.3 Proofs of Results in Section 2.8	183	(12)
B Proofs of Results in Chapter 3	195	(18)
B.1 Proofs of Results in Section 3.1	195	(2)
B.2 Proofs of Results in Section 3.3	197	(5)
B.3 Proofs of Results in Section 3.6	202	(11)
C Proofs of Results in Chapter 4	213	(10)
C.1 Proofs of Results in Section 4.3	213	(6)
C.2 Proofs of Results in Section 4.4	219	(4)
D Proofs of Results in Chapter 5	223	(10)
D.1 Proofs of Results in Section 5.2	223	(3)
D.2 Proofs of Results in Section 5.4	226	(1)
D.3 The Proof of Theorem 5.12	227	(6)
E Proofs of Results in Chapter 6	233	(4)
F Catalogue of Notation	237