Type and Effect Systems

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.

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

What is included with this book?

The New copy of this book will include any supplemental materials advertised. Please check the title of the book to determine if it should include any access cards, study guides, lab manuals, CDs, etc.

The Used, Rental and eBook copies of this book are not guaranteed to include any supplemental materials. Typically, only the book itself is included. This is true even if the title states it includes any access cards, study guides, lab manuals, CDs, etc.

FREE SHIPPING

Rent More, Save More! Use code: BBRENTAL

5% off 1 book, 7% off 2 books, 10% off 3+ books

Type and Effect Systems

Summary

Table of Contents

Supplemental Materials

FREE SHIPPING

Rent More, Save More! Use code: BBRENTAL

5% off 1 book, 7% off 2 books, 10% off 3+ books

Type and Effect Systems

Summary

Table of Contents

Supplemental Materials

Digital License