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