Design concepts in programming languages

Cover
Title Page
Copyright Page
Brief Contents
Table of Contents
Preface
Acknowledgements
I Foundations
1 Introduction
1.1 Programming Languages
1.2 Syntax, Semantics, and Pragmatics
1.3 Goals
1.4 PostFix: A Simple Stack Language
1.4.1 Syntax
1.4.2 Semantics
1.4.3 The Pitfalls of Informal Descriptions
1.5 Overview of the Book
2 Syntax
2.1 Abstract Syntax
2.2 Concrete Syntax
2.3 S-Expression Grammars Specify ASTs
2.3.1 S-Expressions
2.3.2 The Structure of S-Expression Grammars
2.3.3 Phrase Tags
2.3.4 Sequence Patterns
2.3.5 Notational Conventions
2.3.6 Mathematical Foundation of Syntactic Domains
2.4 The Syntax of PostFix
3 Operational Semantics
3.1 The Operational Semantics Game
3.2 Small-step Operational Semantics (SOS)
3.2.1 Formal Framework
3.2.2 Example: An SOS for PostFix
3.2.3 Rewrite Rules
3.2.4 Operational Execution
3.2.5 Progress Rules
3.2.6 Context-based Semantics
3.3 Big-step Operational Semantics
3.4 Operational Reasoning
3.5 Deterministic Behavior of EL
3.6 Termination of PostFix Programs
3.6.1 Energy
3.6.2 The Proof of Termination
3.6.3 Structural Induction
3.7 Safe PostFix Transformations
3.7.1 Observational Equivalence
3.7.2 Transform Equivalence
3.7.3 Transform Equivalence Implies Observational Equivalence
3.8 Extending PostFix
4 Denotational Semantics
4.1 The Denotational Semantics Game
4.2 A Denotational Semantics for EL
4.2.1 Step 1: Restricted ELMM
4.2.2 Step 2: Full ELMM
4.2.3 Step 3: ELM
4.2.4 Step 4: EL
4.2.5 A Denotational Semantics Is Not a Program
4.3 A Denotational Semantics for PostFix
4.3.1 A Semantic Algebra for PostFix
4.3.2 A Meaning Function for PostFix
4.3.3 Semantic Functions for PostFix: the Details
4.4 Denotational Reasoning
4.4.1 Program Equality
4.4.2 Safe Transformations: A Denotational Approach
4.4.3 Technical Difficulties
4.5 Relating Operational and Denotational Semantics
4.5.1 Soundness
4.5.2 Adequacy
4.5.3 Full Abstraction
4.5.4 Operational versus Denotational: A Comparison
5 Fixed Points
5.1 The Fixed Point Game
5.1.1 Recursive Definitions
5.1.2 Fixed Points
5.1.3 The Iterative Fixed Point Technique
5.2 Fixed Point Machinery
5.2.1 Partial Orders
5.2.2 Complete Partial Orders (CPOs)
5.2.3 Pointedness
5.2.4 Monotonicity and Continuity
5.2.5 The Least Fixed Point Theorem
5.2.6 Fixed Point Examples
5.2.7 Continuity and Strictness
5.3 Reflexive Domains
5.4 Summary
II Dynamic Semantics
6 FL: A Functional Language
6.1 Decomposing Language Descriptions
6.2 The Structure of FL
6.2.1 FLK: The Kernel of the FL Language
6.2.2 FL Syntactic Sugar
6.2.3 The FL Standard Library
6.2.4 Examples
6.3 Variables and Substitution
6.3.1 Terminology
6.3.2 Abstract Syntax DAGs and Stoy Diagrams
6.3.3 Alpha-Equivalence
6.3.4 Renaming and Variable Capture
6.3.5 Substitution
6.4 An Operational Semantics for FLK
6.4.1 FLK Evaluation
6.4.2 FLK Simplification
6.5 A Denotational Semantics for FLK
6.5.1 Semantic Algebra
6.5.2 Valuation Functions
6.6 The Lambda Calculus
6.6.1 Syntax of the Lambda Calculus
6.6.2 Operational Semantics of the Lambda Calculus
6.6.3 Denotational Semantics of the Lambda Calculus
6.6.4 Representational Games
7 Naming
7.1 Parameter Passing
7.1.1 Call-by-Name vs. Call-by-Value: The Operational View
7.1.2 Call-by-Name vs. Call-by-Value: The Denotational View
7.1.3 Nonstrict versus Strict Pairs
7.1.4 Handling rec in a CBV Language
7.1.5 Thunking
7.1.6 Call-by-Denotation
7.2 Name Control
7.2.1 Hierarchical Scoping: Static and Dynamic
7.2.2 Multiple Namespaces
7.2.3 Nonhierarchical Scope
7.3 Object-oriented Programming
7.3.1 HOOK: An Object-oriented Kernel
7.3.2 HOOPLA
7.3.3 Semantics of HOOK
8 State
8.1 FL Is a Stateless Language
8.2 Simulating State in FL
8.2.1 Iteration
8.2.2 Single-Threaded Data Flow
8.2.3 Monadic Style
8.2.4 Imperative Programming
8.3 Mutable Data: FLIC
8.3.1 Mutable Cells
8.3.2 Examples of Imperative Programming
8.3.3 An Operational Semantics for FLICK
8.3.4 A Denotational Semantics for FLICK
8.3.5 Call-by-Name versus Call-by-Value Revisited
8.3.6 Referential Transparency, Interference, and Purity
8.4 Mutable Variables: FLAVAR
8.4.1 Mutable Variables
8.4.2 FLAVAR
8.4.3 Parameter-passing Mechanisms for FLAVAR
9 Control
9.1 Motivation: Control Contexts and Continuations
9.2 Using Procedures to Model Control
9.2.1 Representing Continuations as Procedures
9.2.2 Continuation-Passing Style (CPS)
9.2.3 Multiple-value Returns
9.2.4 Nonlocal Exits
9.2.5 Coroutines
9.2.6 Error Handling
9.2.7 Backtracking
9.3 Continuation-based Semantics of FLICK
9.3.1 A Standard Semantics of FLICK
9.3.2 A Computation-based Continuation Semantics of FLICK
9.4 Nonlocal Exits
9.4.1 label and jump
9.4.2 A Denotational Semantics for label and jump
9.4.3 An Operational Semantics for label and jump
9.4.4 call-with-current-continuation (cwcc)
9.5 Iterators: A Simple Coroutining Mechanism
9.6 Exception Handling
9.6.1 raise, handle, and trap
9.6.2 A Standard Semantics for Exceptions
9.6.3 A Computation-based Semantics for Exceptions
9.6.4 A Desugaring-based Implementation of Exceptions
9.6.5 Examples Revisited
10 Data
10.1 Products
10.1.1 Positional Products
10.1.2 Named Products
10.1.3 Nonstrict Products
10.1.4 Mutable Products
10.2 Sums
10.3 Sum of Products
10.4 Data Declarations
10.5 Pattern Matching
10.5.1 Introduction to Pattern Matching
10.5.2 A Desugaring-based Semantics of match
10.5.3 Views
III Static Semantics
11 Simple Types
11.1 Static Semantics
11.2 What Is a Type?
11.3 Dimensions of Types
11.3.1 Dynamic versus Static Types
11.3.2 Explicit versus Implicit Types
11.3.3 Simple versus Expressive Types
11.4 μFLEX: A Language with Explicit Types
11.4.1 Types
11.4.2 Expressions
11.4.3 Programs and Syntactic Sugar
11.4.4 Free Identifiers and Substitution
11.5 Type Checking in μFLEX
11.5.1 Introduction to Type Checking
11.5.2 Type Environments
11.5.3 Type Rules for μFLEX
11.5.4 Type Derivations
11.5.5 Monomorphism
11.6 Type Soundness
11.6.1 What Is Type Soundness?
11.6.2 An Operational Semantics for μFLEX
11.6.3 Type Soundness of μFLEX
11.7 Types and Strong Normalization
11.8 Full FLEX: Typed Data and Recursive Types
11.8.1 Typed Products
11.8.2 Type Equivalence
11.8.3 Typed Mutable Data
11.8.4 Typed Sums
11.8.5 Typed Lists
11.8.6 Recursive Types
11.8.7 Full FLEX Summary
12 Polymorphism and Higher-order Types
12.1 Subtyping
12.1.1 FLEX/S: FLEX with Subtyping
12.1.2 Dimensions of Subtyping
12.1.3 Subtyping and Inheritance
12.2 Polymorphic Types
12.2.1 Monomorphic Types Are Not Expressive
12.2.2 Universal Polymorphism: FLEX/SP
12.2.3 Deconstructible Data Types
12.2.4 Bounded Quantification
12.2.5 Ad Hoc Polymorphism
12.3 Higher-order Types: Descriptions and Kinds
12.3.1 Descriptions: FLEX/SPD
12.3.2 Kinds and Kind Checking: FLEX/SPDK
12.3.3 Discussion
13 Type Reconstruction
13.1 Introduction
13.2 μFLARE: A Language with Implicit Types
13.2.1 μFLARE Syntax and Type Erasure
13.2.2 Static Semantics of μFLARE
13.2.3 Dynamic Semantics and Type Soundness of μFLARE
13.3 Type Reconstruction for μFLARE
13.3.1 Type Substitutions
13.3.2 Unification
13.3.3 The Type-Constraint-Set Abstraction
13.3.4 A Reconstruction Algorithm for μFLARE
13.4 Let Polymorphism
13.4.1 Motivation
13.4.2 A μFLARE Type System with Let Polymorphism
13.4.3 μFLARE Type Reconstruction with Let Polymorphism
13.5 Extensions
13.5.1 The Full FLARE Language
13.5.2 Mutable Variables
13.5.3 Products and Sums
13.5.4 Sum-of-products Data Types
14 Abstract Types
14.1 Data Abstraction
14.1.1 A Point Abstraction
14.1.2 Procedural Abstraction Is Not Enough
14.2 Dynamic Locks and Keys
14.3 Existential Types
14.4 Nonce Types
14.5 Dependent Types
14.5.1 A Dependent Package System
14.5.2 Design Issues with Dependent Types
15 Modules
15.1 An Overview of Modules and Linking
15.2 An Introduction to FLEX/M
15.3 Module Examples: Environments and Tables
15.4 Static Semantics of FLEX/M Modules
15.4.1 Scoping
15.4.2 Type Equivalence
15.4.3 Subtyping
15.4.4 Type Rules
15.4.5 Implicit Projection
15.4.6 Typed Pattern Matching
15.5 Dynamic Semantics of FLEX/M Modules
15.6 Loading Modules
15.6.1 Type Soundness of load via a Load-Time Check
15.6.2 Type Soundness of load via a Compile-Time Check
15.6.3 Referential Transparency of load for File-Value Coherence
15.7 Discussion
15.7.1 Scoping Limitations
15.7.2 Lack of Transparent and Translucent Types
15.7.3 The Coherence Problem
15.7.4 Purity Issues
16 Effects Describe Program Behavior
16.1 Types, Effects, and Regions: What, How, and Where
16.2 A Language with a Simple Effect System
16.2.1 Types, Effects, and Regions
16.2.2 Type and Effect Rules
16.2.3 Reconstructing Types and Effects: Algorithm Z
16.2.4 Effect Masking Hides Unobservable Effects
16.2.5 Effect-based Purity for Generalization
16.3 Using Effects to Analyze Program Behavior
16.3.1 Control Transfers
16.3.2 Dynamic Variables
16.3.3 Exceptions
16.3.4 Execution Cost Analysis
16.3.5 Storage Deallocation and Lifetime Analysis
16.3.6 Control Flow Analysis
16.3.7 Concurrent Behavior
16.3.8 Mobile Code Security
IV Pragmatics
17 Compilation
17.1 Why Do We Study Compilation?
17.2 Tortoise Architecture
17.2.1 Overview of Tortoise
17.2.2 The Compiler Source Language: FLARE/V
17.2.3 Purely Structural Transformations
17.3 Transformation 1: Desugaring
17.4 Transformation 2: Globalization
17.5 Transformation 3: Assignment Conversion
17.6 Transformation 4: Type/Effect Reconstruction
17.6.1 Propagating Type and Effect Information
17.6.2 Effect-based Code Optimization
17.7 Transformation 5: Translation
17.7.1 The Compiler Intermediate Language: FIL
17.7.2 Translating FLARE to FIL
17.8 Transformation 6: Renaming
17.9 Transformation 7: CPS Conversion
17.9.1 The Structure of Tortoise CPS Code
17.9.2 A Simple CPS Transformation
17.9.3 A More Efficient CPS Transformation
17.9.4 CPS-Converting Control Constructs
17.10 Transformation 8: Closure Conversion
17.10.1Flat Closures
17.10.2Variations on Flat Closure Conversion
17.10.3Linked Environments
17.11 Transformation 9: Lifting
17.12 Transformation 10: Register Allocation
17.12.1The FILreg Language
17.12.2A Register Allocation Algorithm
17.12.3The Expansion Phase
17.12.4The Register Conversion Phase
17.12.5The Spilling Phase
18 Garbage Collection
18.1 Why Garbage Collection?
18.2 FRM: The FIL Register Machine
18.2.1 The FRM Architecture
18.2.2 FRM Descriptors
18.2.3 FRM Blocks
18.3 A Block Is Dead if It Is Unreachable
18.3.1 Reference Counting
18.3.2 Memory Tracing
18.4 Stop-and-copy GC
18.5 Garbage Collection Variants
18.5.1 Mark-sweep GC
18.5.2 Tag-free GC
18.5.3 Conservative GC
18.5.4 Other Variations
18.6 Static Approaches to Automatic Deallocation
A A Metalanguage
A.1 The Basics
A.1.1 Sets
A.1.2 Boolean Operators and Predicates
A.1.3 Tuples
A.1.4 Relations
A.2 Functions
A.2.1 What Is a Function?
A.2.2 Application
A.2.3 More Function Terminology
A.2.4 Higher-order Functions
A.2.5 Multiple Arguments and Results
A.2.6 Lambda Notation
A.2.7 Recursion
A.2.8 Lambda Notation Is Not Lisp!
A.3 Domains
A.3.1 Motivation
A.3.2 Types
A.3.3 Product Domains
A.3.4 Sum Domains
A.3.5 Sequence Domains
A.3.6 Function Domains
A.4 Metalanguage Summary
A.4.1 The Metalanguage Kernel
A.4.2 The Metalanguage Sugar
B Our Pedagogical Languages
References
Index