The Optimal Implementation of Functional Programming Languages

1 Introduction
	1.0.1 How to read this book
2 Optimal Reduction
	2.1 Some Sharing mechanisms
		2.1.1 Wadsworth's technique
		2.1.2 Combinators
		2.1.3 Environment Machines
	2.2 Sharing graphs
		2.2.1 Graph rewriting
		2.2.2 Read-back and Semantics
3 The full algorithm
	3.1 Pairing fans
	3.2 Sharing Graphs
	3.3 The initial encoding of λ-terms
	3.4 Lamping's paths
		3.4.1 Contexts and proper paths
	3.5 Correctness of the algorithm
		3.5.1 Properties of sharing graphs
		3.5.2 Correspondence between sharing graphs and λ-terms
		3.5.3 Expanded proper paths
		3.5.4 Proof of Theorem 3.5.15 (correctness)
		3.5.5 Proof of Lemma 3.5.17 (properties of expanded proper paths)
		3.5.6 Proof of the sharing graph properties
4 Optimal Reductions and Linear Logic
	4.1 Intuitionistic Linear Logic
	4.2 The "!" modality
		4.2.1 Boxes
		4.2.2 A Remark for Categoricians
	4.3 The duplication problem
5 Redex Families and Optimality
	5.1 Zig-Zag
		5.1.1 Permutation equivalence
		5.1.2 Families of redexes
	5.2 Extraction
		5.2.1 Extraction and families
	5.3 Labeling
		5.3.1 Confluence and Standardization
		5.3.2 Labeled and unlabeled λ-calculus
		5.3.3 Labeling and families
	5.4 Reduction by families
		5.4.1 Complete derivations
	5.5 Completeness of Lamping's algorithm
	5.6 Optimal derivations
6 Paths
	6.1 Several definitions of paths
	6.2 Legal Paths
		6.2.1 Reminder on labeled λ-calculus
		6.2.2 Labels and paths
		6.2.3 The equivalence between extraction and labeling
		6.2.4 Well balanced paths and legal paths
		6.2.5 Legal paths and redex families
		6.2.6 Legal paths and optimal reductions
	6.3 Consistent Paths
		6.3.1 Reminder on proper paths
		6.3.2 Consistency
	6.4 Regular Paths
		6.4.1 The Dynamic Algebra ℒ?
		6.4.2 A model
		6.4.3 Virtual Reduction
	6.5 Relating Paths
		6.5.1 Discriminants
		6.5.2 Legal paths are regular and vice-versa
		6.5.3 Consistent paths are regular and vice-versa
	6.6 Virtual interactions
		6.6.1 Residuals and ancestors of consistent paths
		6.6.2 Fan annihilations and cycles
7 Read-back
	7.1 Static and dynamic sharing
		7.1.1 Grouping sequences of brackets
		7.1.2 Indexed λ-trees
		7.1.3 Beta rule
		7.1.4 Multiplexer
	7.2 The propagation rules
		7.2.1 Mux interactions
		7.2.2 Mux propagation rules
		7.2.3 The absorption rule
		7.2.4 Redexes
	7.3 Deadlocked redexes
		7.3.1 Critical pairs
		7.3.2 Mux permutation equivalence
	7.4 Sharing morphisms
		7.4.1 Simulation lemma
	7.5 Unshared beta reduction
	7.6 Paths
	7.7 Algebraic semantics
		7.7.1 Left inverses of lifting operators
		7.7.2 The inverse semigroup LSeq*
	7.8 Proper paths
		7.8.1 Deadlock-freeness and properness
	7.9 Soundness and adequateness
	7.10 Read-back and optimality
8 Other translations in Sharing Graphs
	8.1 Introduction
	8.2 The bus notation
	8.3 The bus notation of the translation ℱ
	8.4 The correspondence of ℱ and ?
	8.5 Concluding remarks
9 Safe Nodes
	9.1 Accumulation of control operators
	9.2 Eliminating redundant information
	9.3 Safe rules
	9.4 Safe Operators
	9.5 Examples and Benchmarks
10 Complexity
	10.1 The simply typed case
		10.1.1 Typing Lamping's rules
		10.1.2 The η-expansion method
		10.1.3 Simulating generic elementary-time bounded computation
	10.2 Superposition and higher-order sharing
		10.2.1 Superposition
		10.2.2 Higher-order sharing
	10.3 Conclusions
11 Functional Programming
	11.1 Interaction Systems
		11.1.1 The Intuitionistic Nature of Interaction Systems
	11.2 Sharing Graphs Implementation
		11.2.1 The encoding of IS-expressions
		11.2.2 The translation of rewriting rules
12 The Bologna Optimal Higher-order Machine
	12.1 Source Language
	12.2 Reduction
		12.2.1 Graph Encoding
		12.2.2 Graph Reduction
	12.3 Garbage Collection
		12.3.1 Implementation Issues
		12.3.2 Examples and Benchmarks
	12.4 Problems
		12.4.1 The case of "append"
Bibliography