Type and Effect Systems

The following sections are included:

• Contents

• List of Figures

• Preface

The following sections are included:

• Basic Concepts

• Polymorphism
  • An Inference System
  • An Inference Algorithm
  • Implicit Treatments of Side Effects

• An Inference System for Effects
  • Effects Controlling Polymorphism
  • Regions
  • Behaviours
  • Subeffecting

• An Inference Algorithm for Effects
  • Effect Constraints
  • Solving Effect Constraints
  • Downwards Closure for Polymorphism

• Shape Conformant Subtyping with Effects
  • Inference Systems for Atomic Subtyping
  • Algorithmic Techniques for Atomic Subtyping
  • Integrating Shape Conformant Subtyping

• Overview of the Development
  • The Main Ideas
  • A Prototype Implementation
  • Benchmarks
  • A Reader's Guide to the Book

The following sections are included:

• The Source Language
  • Concurrent Programming

• Basic Notions
  • Regions
  • Behaviours
  • Types
  • Constraints
  • Miscellaneous

• Shape Conformant Subtyping
  • The Ordering on Behaviours
  • The Ordering on Types

• The Type Inference System

• The Rule for Generalisation
  • Backwards Closure
  • The Arrow Relation
  • Well-formed Type Schemes

• Pragmatics
  • Basic Results
  • Trace Inclusion
  • Normalisation of Inference Trees

• Conservative Extension of Hindley-Milner

The following sections are included:

• The Sequential Semantics

• The Concurrent Semantics

• Reasoning about Inference Trees

• Sequential Soundness

• Erroneous Programs cannot be Typed

• Concurrent Soundness

The following sections are included:

• Algorithm W′

• Algorithm ℱ
  • Termination and Soundness

• Algorithm ℛ
  • Termination and Soundness
  • Confluence Properties

• Syntactic Soundness of Algorithm W
  • The Relation to Hindley-Milner Typing

The following sections are included:

• The Completeness Result for Programs
  • Applicability of the Completeness Result
  • The Relation to Hindley-Milner Typing

• Completeness of Algorithm ℱ

• Completeness of Algorithm ℛ

• Lazy Instance for Type Schemes

• The Completeness Result for Expressions
  • The Proof: Lifting from W′ to W
  • The Proof: The Case for Type Schemes
  • The Proof: The Case for Types

The following sections are included:

• Solving Region Constraints

• A Catalogue of Behaviour Transformations
  • Simplification
  • Hiding
  • Unfolding
  • Collapsing

• The Notion of Bisimulation

• Correctness of the Transformations
  • Simplification
  • Hiding
  • Unfolding
  • Collapsing

• A Subject Reduction Property

• Semantic Soundness of a Post-processing W

The following sections are included:

• The Production Cell
  • Safety Conditions for the Table
  • An Implementation of the Table
  • The Behaviour of the Table

• Validating the Safety Conditions
  • Vertical Bounds for the Table
  • Horizontal Bounds for the Table
  • No Collisions on the Table

• Discussion

The following sections are included:

• Appendix A Proofs of Results in Chapter 2

• Appendix B Proofs of Results in Chapter 3

• Appendix C Proofs of Results in Chapter 4

• Appendix D Proofs of Results in Chapter 5

• Appendix E Proofs of Results in Chapter 6

• Appendix F A Catalogue of Notation

• Index

• Bibliography