Table of contents for Design concepts in programming languages / Franklyn A. Turbak and David K. Gifford, with Mark A. Sheldon.

Bibliographic record and links to related information available from the Library of Congress catalog.

Note: Contents data are machine generated based on pre-publication provided by the publisher. Contents may have variations from the printed book or be incomplete or contain other coding.


Counter
Contents
Contents 	ii
Preface 	xiii
Acknowledgments 	xv
I Foundations 	1
1 Introduction 	3
1.1 Programming Languages 	3
1.2 Syntax, Semantics, and Pragmatics 	4
1.3 Goals 	6
1.4 PostFix: A Simple Stack Language 	7
1.4.1 Syntax 	8
1.4.2 Semantics 	8
1.4.3 The Pitfalls of Informal Descriptions 	13
1.5 Overview of the Book 	14
2 Syntax 	19
2.1 Abstract Syntax 	20
2.2 Concrete Syntax 	22
2.3 S-Expression Grammars Specify ASTs 	23
2.3.1 S-Expressions 	23
2.3.2 The Structure of S-Expression Grammars 	24
2.3.3 Phrase Tags 	29
2.3.4 Sequence Patterns 	30
2.3.5 Notational Conventions 	32
2.3.6 Mathematical 	37
3 Operational Semantics 	43
3.1 The Operational Semantics Game 	43
3.2 Small-step Operational Semantics (SOS) 	47
3.2.1 Formal Framework 	47
3.2.2 Example: An SOS for PostFix 	49
3.2.3 Rewrite Rules 	51
3.2.4 Operational Execution 	55
3.2.5 Progress Rules 	59
3.2.6 Context-based Semantics 	67
3.3 Big-step Operational Semantics 	69
3.4 Operational Reasoning 	74
3.5 Deterministic Behavior of EL 	76
3.6 Termination of PostFix Programs 	79
3.6.1 Energy 	79
3.6.2 The Proof of Termination 	81
3.6.3 Structural Induction 	82
3.7 Safe PostFix Transformations 	84
3.7.1 Observational Equivalence 	84
3.7.2 Transform Equivalence 	86
3.7.3 Transform Equivalence Implies Observational Equivalence 90
3.8 Extending PostFix 	94
4 Denotational Semantics 	107
4.1 The Denotational Semantics Game 	107
4.2 A Denotational Semantics for EL 	111
4.2.1 Step 1: Restricted ELMM 	111
4.2.2 Step 2: Full ELMM 	113
4.2.3 Step 3: ELM 	117
4.2.4 Step 4: EL 	120
4.2.5 A Denotational Semantics is Not a Program 	121
4.3 A Denotational Semantics for PostFix 	124
4.3.1 A Semantic Algebra for PostFix 	124
4.3.2 A Meaning Function for PostFix 	127
4.3.3 Semantic Functions for PostFix: the Details 	134
4.4 Denotational Reasoning 	137
4.4.1 Program Equality 	137
4.4.2 Safe Transformations: A Denotational Approach 	138
4.4.3 Technical Di_culties 	141
4.5 Relating Operational and Denotational Semantics 	142
4.5.1 Soundness 	142
4.5.2 Adequacy 	148
4.5.3 Full Abstraction 	149
4.5.4 Operational vs. Denotational: A Comparison 	151
5 Fixed Points	153
5.1 The Fixed Point Game 	153
5.1.1 Recursive De_nitions 	153
5.1.2 Fixed Points 	156
5.1.3 The Iterative Fixed Point Technique 	158
5.2 Fixed Point Machinery 	163
5.2.1 Partial Orders 	163
5.2.2 Complete Partial Orders (CPOs) 	170
5.2.3 Pointedness 	173
5.2.4 Monotonicity and Continuity 	175
5.2.5 The Least Fixed Point Theorem 	178
5.2.6 Fixed Point Examples	179
5.2.7 Continuity and Strictness 	184
5.3 Reexive Domains 	187
5.4 Summary 	189
II Dynamic Semantics 	191
6 FL: A Functional Language 	193
6.1 Decomposing Language Descriptions 	193
6.2 The Structure of FL 	194
6.2.1 FLK: The Kernel of the FL Language 	195
6.2.2 FL Syntactic Sugar 	203
6.2.3 The FL Standard Library 	218
6.2.4 Examples 	221
6.3 Variables and Substitution 	227
6.3.1 Terminology 	227
6.3.2 Abstract Syntax DAGs and Stoy Diagrams 	230
6.3.3 Alpha-Equivalence 	233
6.3.4 Renaming and Variable Capture 	233
6.3.5 Substitution 	235
6.4 An Operational Semantics for FLK 	239
6.4.1 FLK Evaluation 	239
6.4.2 FLK Simpli_cation 	250
6.5 A Denotational Semantics for FLK 	255
6.5.1 Semantic Algebra 	255
6.5.2 Valuation Functions 	260
6.6 The Lambda Calculus 	269
6.6.1 Syntax of the Lambda 	270
6.6.2 Operational Semantics of the Lambda Calculus 	271
6.6.3 Denotational Semantics 	276
7 Naming 	285
7.1 Parameter Passing 	287
7.1.1 Call-by-Name vs. Call-by-Value: The Operational View 288
7.1.2 Call-by-Name vs. Call-by-Value: The Denotational View 293
7.1.3 Nonstrict vs. Strict Pairs 	295
7.1.4 Handling rec in a CBV Language 	298
7.1.5 Thunking 	301
7.1.6 Call-by-Denotation 	304
7.2 Name Control 	308
7.2.1 Hierarchical Scoping: Static and Dynamic 	309
7.2.2 Multiple Namespaces 	322
7.2.3 Nonhierarchical Scope 	325
7.3 Object-Oriented Programming 	333
7.3.1 HOOK: An Object-oriented Kernel 	335
7.3.2 HOOPLA 	341
7.3.3 Semantics of HOOK 	343
8 State 	351
8.1 FL is a Stateless Language 	352
8.2 Simulating State In FL 	357
8.2.1 Iteration 	358
8.2.2 Single-Threaded Data Flow 	359
8.2.3 Monadic Style 	361
8.2.4 Imperative Programming 	364
8.3 Mutable Data: FLIC 	365
8.3.1 Mutable Cells 	365
8.3.2 Examples of Imperative Programming 	368
8.3.3 An Operational Semantics for FLICK 	372
8.3.4 A Denotational Semantics for FLICK 	378
8.3.5 Call-by-Name vs. Call-by-Value Revisited 	390
8.3.6 Referential Transparency, Interference, and Purity 	391
8.4 Mutable Variables: FLAVAR 	394
8.4.1 Mutable Variables 	
8.4.2 FLAVAR 	395
8.4.3 Parameter-passing Mechanisms for FLAVAR 	396
9 Control 	405
9.1 Motivation: Control Contexts and Continuations 	405
9.2 Using Procedures to Model Control 	408
9.2.1 Representing Continuations as Procedures 	408
9.2.2 Continuation-Passing Style (CPS) 	411
9.2.3 Multiple-value Returns 	412
9.2.4 Nonlocal Exits 	415
9.2.5 Coroutines 	418
9.2.6 Error Handling 	420
9.2.7 Backtracking 	425
9.3 Continuation-Based Semantics of FLICK 	431
9.3.1 A Standard Semantics of	. 432
9.3.2 A Computation-based Continuation Semantics of FLICK 441
9.4 Nonlocal Exits 	451
9.4.1 label and jump 	451
9.4.2 A Denotational Semantics for label and jump 	455
9.4.3 An Operational Semantics for label and jump 	460
9.4.4 call-with-current-continuation (cwcc) 	461
9.5 Iterators: A Simple Coroutining Mechanism 	463
9.6 Exception Handling 	470
9.6.1 raise, handle, and trap 	471
9.6.2 A Standard Semantics for Exceptions 	475
9.6.3 A Computation-based Semantics for Exceptions 	480
9.6.4 A Desugaring-based Implementation of Exceptions 	483
9.6.5 Examples Revisited 	485
10 Data 	495
10.1 Products 	495
10.1.1 Positional Products 	496
10.1.2 Named Products 	504
10.1.3 Nonstrict Products 	506
10.1.4 Mutable Products 	516
10.2 Sums 	521
10.3 Sum of Products 	530
10.4 Data Declarations 	535
10.5 Pattern Matching 	542
10.5.1 Introduction to Pattern Matching	542
10.5.2 A Desugaring-based Semantics of match 	547
10.5.3 Views 	557
III Static Semantics 	565
11 Simple Types 	567
11.1 Static Semantics 	567
11.2 What is a Type? 	570
11.3 Dimensions of Types 	572
11.3.1 Dynamic versus Static Types 	572
11.3.2 Explicit versus Implicit Types	574
11.3.3 Simple versus Expressive Types 	576
11.4 _FLEX: A Language with Explicit Types 	577
11.4.1 Types 	577
11.4.2 Expressions 	579
11.4.3 Programs and Syntactic Sugar 	582
11.4.4 Free Identi_ers and Substitution 	585
11.5 Type Checking in _FLEX 	589
11.5.1 Introduction to Type Checking 	589
11.5.2 Type Environments 	590
11.5.3 Type Rules for _FLEX 	591
11.5.4 Type Derivations 	595
11.5.5 Monomorphism 	601
11.6 Type Soundness 	606
11.6.1 What is Type Soundness? 	606
11.6.2 An Operational Semantics for _FLEX 	608
11.6.3 Type Soundness of _FLEX 	612
11.7 Types and Strong Normalization 	617
11.8 Full FLEX: Typed Data and Recursive Types 	619
11.8.1 Typed Products 	619
11.8.2 Type Equivalence	623
11.8.3 Typed Mutable Data 	624
11.8.4 Typed Sums 	626
11.8.5 Typed Lists 	628
11.8.6 Recursive Types 	631
11.8.7 Full FLEX Summary 	638
12 Polymorphism and Higher-Order Types 	643
12.1 Subtyping	643
12.1.1 FLEX/S: FLEX with Subtyping 	644
12.1.2 Dimensions of Subtyping 	654
12.1.3 Subtyping and Inheritance 	664
12.2 Polymorphic Types 	666
12.2.1 Monomorphic Types are Not Expressive 	666
12.2.2 Universal Polymorphism: FLEX/SP 	667
12.2.3 Deconstructible Data Types 	677
12.2.4 Bounded Quanti_cation 	684
12.2.5 Ad Hoc Polymorphism 	685
12.3 Higher-Order Types: Descriptions and Kinds 	688
12.3.1 Descriptions: FLEX/SPD 	688
12.3.2 Kinds and Kind Checking: FLEX/SPDK 	696
12.3.3 Discussion 	701
13 Type 	707
13.2 _FLARE: A Language with Implicit Types 	710
13.2.1 _FLARE Syntax and Type Erasure 	710
13.2.2 Static Semantics of _	712
13.2.3 Dynamic Semantics and Type Soundness of _FLARE 714
13.3 Type Reconstruction for _FLARE 	718
13.3.1 Type Substitutions 	719
13.3.2 Uni_cation 	720
13.3.3 The Type-Constraint-Set Abstraction 	723
13.3.4 A Reconstruction Algorithm for _FLARE 	727
13.4 Let Polymorphism 	736
13.4.1 Motivation 	736
13.4.2 A _FLARE Type System with Let Polymorphism 	738
13.4.3 _FLARE Type Reconstruction with Let Polymorphism 742
13.5 Extensions	. 747
13.5.1 The Full FLARE Language	747
13.5.2 Mutable Variables 	752
13.5.3 Products and Sums 	755
13.5.4 Sum-of-products Data Types 	759
14 Abstract Types 	769
14.1 Data Abstraction 	769
14.1.1 A Point Abstraction 	770
14.1.2 Procedural Abstraction Is Not Enough 	771
14.2 Dynamic Locks and Keys 	773
14.3 Existential Types 	777
14.4 Nonce Types 	788
14.5 Dependent Types 	797
14.5.1 A Dependent Package System 	797
14.5.2 Design Issues with Dependent Types 	804
15 Modules 	813
15.1 An Overview of Modules and Linking 	813
15.2 An Introduction to FLEX/M 	815
15.3 Module Examples: Environments and Tables 	824
15.4 Static Semantics of FLEX/M Modules 	832
15.4.1 Scoping 	833
15.4.3 Subtyping 	834
15.4.4 Type Rules 	835
15.4.5 Implicit Projection 	839
15.4.6 Typed Pattern Matching 	842
15.5 Dynamic Semantics of FLEX/M Modules 	844
15.6 Loading Modules 	845
15.6.1 Type Soundness of load Via a Load-Time Check 	847
15.6.2 Type Soundness of load Via a Compile-Time Check 	848
15.6.3 Referential Transparency of load for File-Value Coherence 850
15.7 Discussion 	852
15.7.1 Scoping Limitations 	852
15.7.2 Lack of Transparent and Translucent Types 	853
15.7.3 The Coherence Problem 	855
15.7.4 Purity Issues 	857
16 E_ects Describe Program Behavior 	861
16.1 Types, E_ects, and Regions: What, How, and Where 	861
16.2 A Language with a Simple E_ect System 	863
16.2.1 Types, E_ects, and Regions 	863
16.2.2 Type and E_ect Rules 	868
16.2.3 Reconstructing Types and E_ects: Algorithm Z 	876
16.2.4 E_ect Masking Hides Unobservable E_ects 	887
16.2.5 E_ect-based Purity for Generalization 	889
16.3 Using E_ects to Analyze Program Behavior 	894
16.3.1 Control Transfers 	898
16.3.3 Exceptions 	900
16.3.4 Execution Cost Analysis 	903
16.3.5 Storage Deallocation and Lifetime Analysis 	905
16.3.6 Control Flow Analysis 	909
16.3.7 Concurrent Behavior 	910
16.3.8 Mobile Code Security 	913
IV Pragmatics 	915
17 Compilation 	917
17.1 Why do we study compilation? 	917
17.2 Tortoise Architecture 	918
17.2.1 Overview of Tortoise 	918
17.2.2 The Compiler Source Language: FLARE/V 	919
17.2.3 Purely Structural Transformations 	923
17.3 Transformation 1: Desugaring 	925
17.4 Transformation 2: Globalization 	925
17.5 Transformation 3: Assignment Conversion 	931
17.6 Transformation 4: Type/E_ect Reconstruction 	936
17.6.1 Propagating Type and E_ect Information 	936
17.6.2 E_ect-based Code 	937
17.7 Transformation 5: Translation 	940
17.7.1 The Compiler Intermediate Language: FIL 	940
17.7.2 Translating FLARE to FIL 	946
17.8 Transformation 6: Renaming 	948
17.9 Transformation 7: CPS Conversion 	951
17.9.1 The Structure of Tortoise CPS Code	953
17.9.2 A Simple CPS Transformation 	958
17.9.3 A More E_cient CPS Transformation 	966
17.9.4 CPS-Converting Control Constructs 	978
17.10 Transformation 8: Closure Conversion 	983
17.10.1 Flat Closures 	984
17.10.2Variations on Flat Closure Conversion 	992
17.10.3 Linked Environments 	996
17.11 Transformation 9: Lifting 	1000
17.12 Transformation 10: Register Allocation 	1002
17.12.1 The FILreg Language 	1004
17.12.2A Register Allocation Algorithm 	1007
17.12.3 The Expansion Phase 	1008
17.12.4 The Register Conversion Phase 	1009
17.12.5 The Spilling Phase 	 1017
18 Garbage Collection 	1023
18.1 Why Garbage Collection? 	1023
18.2 FRM: The FIL Register Machine 	1026
18.2.1 The FRM Architecture 	1026
18.2.2 FRM Descriptors 	1027
18.2.3 FRM Blocks 	1030
18.3 A Block is Dead if it is Unreachable 	1033
18.3.1 Reference Counting 	1034
18.3.2 Memory Tracing 	1035
18.4 Stop-and-copy GC 	1036
18.5 Garbage Collection Variants 	1043
18.5.1 Mark-sweep GC 	1043
18.5.2 Tag-Free GC 	1044
18.5.3 Conservative GC 	1044
18.5.4 Other Variations 	1045
18.6 Static Approaches to Automatic Deallocation 	1046
A A Metalanguage 	1049
A.1 The Basics 	1049
A.1.1 Sets 	1050
A.1.2 Boolean Operators and Predicates 	1052
A.1.3 Tuples 	1054
A.1.4 Relations 	1055
A.2 Functions 	1057
A.2.1 What is a Function? 	1057
A.2.2 Application 	1059
A.2.3 More Function Terminology 	1060
A.2.4 Higher-Order Functions 	1061
A.2.5 Multiple Arguments and Results 	1062
A.2.6 Lambda Notation 	1065
A.2.7 Recursion 	1068
A.2.8 Lambda Notation is not Lisp! 	1069
A.3 Domains 	1071
A.3.1 Motivation 	1071
A.3.2 Types 	1072
A.3.3 Product Domains 	1073
A.3.4 Sum Domains 	1075
A.3.5 Sequence Domains 	1080
A.3.6 Function Domains 	1082
A.4 Metalanguage Summary 	1084
A.4.1 The Metalanguage Kernel 	1085
A.4.2 The Metalanguage Sugar 	1087
B Our Pedagogical Languages 	1095
Bibliography 	1097
Index 	1116

Library of Congress Subject Headings for this publication:

Programming languages (Electronic computers).