Semantics Engineering with PLT Redex
by Felleisen, Flatt, Findler
ISBN: 9780262258173 | Copyright 2009
Instructor Requests
This text is the first comprehensive presentation of reduction semantics in one volume; it also introduces the first reliable and easy-to-use tool set for such forms of semantics. Software engineers have long known that automatic tool support is critical for rapid prototyping and modeling, and this book is addressed to the working semantics engineer (graduate student or professional language designer). The book comes with a prototyping tool suite to develop, explore, test, debug, and publish semantic models of programming languages. With PLT Redex, semanticists can formulate models as grammars and reduction models on their computers with the ease of paper and pencil. The text first presents a framework for the formulation of language models, focusing on equational calculi and abstract machines, then introduces PLT Redex, a suite of software tools for expressing these models as PLT Redex models. Finally, experts describe a range of models formulated in Redex. PLT Redex comes with the PLT Scheme implementation, available free at http://www.plt-scheme.org/. Readers can download the software and experiment with Redex as they work their way through the book.
| Expand/Collapse All | |
|---|---|
| Contents (pg. vii) | |
| Preface (pg. ix) | |
| Organization (pg. ix) | |
| To the Instructor (pg. x) | |
| To the Student (pg. x) | |
| Software (pg. xi) | |
| Acknowledgments (pg. xi) | |
| Part I. Reduction Semantics (pg. 1) | |
| Chapter 1. Semantics via Syntax (pg. 5) | |
| 1·1 Defining Sets. (pg. 5) | |
| 1·2 Relations (pg. 7) | |
| 1·3 Semantics as an Equivalence Relation (pg. 8) | |
| 1·4 Semantics via Reduction (pg. 9) | |
| 1·5 Reduction in Context (pg. 10) | |
| 1·6 Evaluation Functions (pg. 11) | |
| 1·7 Notation Summary (pg. 12) | |
| Chapter 2. Analyzing Syntactic Semantics (pg. 13) | |
| 2·1 From Questions to Mathematical Claims (pg. 13) | |
| 2·2 Answers as Theorems (pg. 14) | |
| Chapter 3. The λ-Calculus (pg. 23) | |
| 3·1 Functions and the λ-Calculus (pg. 23) | |
| 3·2 λ-Calculus: Syntax and Reductions (pg. 25) | |
| 3·3 Encoding Booleans (pg. 29) | |
| 3·4 Encoding Pairs (pg. 30) | |
| 3·5 Encoding Numbers (pg. 31) | |
| 3·6 Encodings and Errors (pg. 33) | |
| 3·7 Recursion (pg. 34) | |
| 3·8 Consistency and Normal Forms (pg. 38) | |
| 3·9 Normal Forms and Reduction Strategies (pg. 40) | |
| 3·10 History (pg. 43) | |
| Chapter 4. ISWIM (pg. 45) | |
| 4·1 ISWIM Expressions (pg. 45) | |
| 4·2 Calculating with ISWIM (pg. 47) | |
| 4·3 Alpha, Eta, and Quotients (pg. 49) | |
| 4·4 The Yv Combinator (pg. 50) | |
| 4·5 Evaluation (pg. 52) | |
| 4·6 Consistency (pg. 52) | |
| 4·7 Observational Equivalence (pg. 58) | |
| 4·8 History (pg. 63) | |
| Chapter 5. An Abstract Syntax Machine (pg. 65) | |
| 5·1 Standard Reductions (pg. 65) | |
| 5·2 The Standard Reduction Theorem (pg. 69) | |
| 5·3 Reasoning about Observational Equivalence (pg. 80) | |
| 5·4 Uniform Evaluation (pg. 84) | |
| 5·5 History (pg. 87) | |
| Chapter 6. Abstract Register Machines (pg. 89) | |
| 6·1 The CC Machine (pg. 89) | |
| 6·2 The SCC Machine (pg. 94) | |
| 6·3 The CK Machine (pg. 99) | |
| 6·4 The CEK Machine (pg. 100) | |
| 6·5 History (pg. 105) | |
| Chapter 7. Tail Calls and More Space Savings (pg. 107) | |
| 7·1 SECD Machine (pg. 107) | |
| 7·2 Space for Evaluation Contexts (pg. 109) | |
| 7·3 Space for Environments (pg. 112) | |
| 7·4 History (pg. 114) | |
| Chapter 8. Control (pg. 115) | |
| 8·1 Error ISWIM (pg. 116) | |
| 8·2 Relating ISWIM and Error ISWIM (pg. 124) | |
| 8·3 Handler ISWIM (pg. 129) | |
| 8·4 Continuation ISWIM and Total Control (pg. 139) | |
| 8·5 History (pg. 144) | |
| Chapter 9. State (pg. 145) | |
| 9·1 Programming in State ISWIM (pg. 146) | |
| 9·2 An Evaluator for State ISWIM (pg. 148) | |
| 9·3 The State ISWIM Calculus (pg. 154) | |
| 9·4 The CESK Machine (pg. 165) | |
| 9·5 Space and Garbage Collection (pg. 167) | |
| 9·6 History (pg. 173) | |
| Chapter 10. Simply Typed ISWIM (pg. 175) | |
| 10·1 Simply Typed ISWIM (pg. 176) | |
| 10·2 Typed Programs Don’t Go Wrong (pg. 186) | |
| 10·3 Types and Recursion (pg. 190) | |
| 10·4 Typed Programs Go to Specific Stuck States (pg. 197) | |
| 10·5 History (pg. 198) | |
| Part II. PLT Redex (pg. 201) | |
| Chapter 11. The Basics (pg. 205) | |
| 11·1 PLT Redex and PLT Scheme (pg. 205) | |
| 11·2 Specifying Abstract Syntax (pg. 207) | |
| 11·3 Specifying Reduction Relations (pg. 210) | |
| 11·4 Tracing (pg. 212) | |
| 11·5 Variation on a Theme (pg. 213) | |
| Chapter 12. Variables and Meta-functions (pg. 217) | |
| 12·1 More on Redex Grammars (pg. 217) | |
| 12·2 Meta-functions (pg. 219) | |
| 12·3 Reductions via with Clauses (pg. 224) | |
| Chapter 13. Layered Development (pg. 227) | |
| 13·1 Extending Languages (pg. 227) | |
| 13·2 Extending Reduction Relations (pg. 230) | |
| 13·3 Side Conditions (pg. 234) | |
| Chapter 14. Testing (pg. 237) | |
| 14·1 Test Cases, Test Suites (pg. 237) | |
| 14·2 Abstracting over Test Cases (pg. 238) | |
| 14·3 Testing Properties (pg. 240) | |
| 14·4 The CK Machine (pg. 241) | |
| Chapter 15. Debugging (pg. 245) | |
| 15·1 Visual Debugging, Take 1 (pg. 245) | |
| 15·2 Type Checking, Take 1 (pg. 248) | |
| 15·3 Visual Debugging, Take 2 (pg. 253) | |
| 15·4 Type Checking, Take 2 (pg. 256) | |
| Chapter 16. Case Study 1 (pg. 259) | |
| 16·1 Adding Mutation (pg. 259) | |
| 16·2 Evaluation Everywhere (pg. 261) | |
| 16·3 R6RS: A First Attempt (pg. 263) | |
| 16·4 R6RS: A Second Attempt (pg. 266) | |
| 16·5 R6RS: Finally (pg. 268) | |
| Chapter 17. Case Study 2 (pg. 271) | |
| 17·1 Continuations as Functions (pg. 271) | |
| 17·2 Continuations as Evaluation Contexts (pg. 273) | |
| Chapter 18. Typesetting (pg. 277) | |
| 18·1 The Defaults (pg. 277) | |
| 18·2 Simple Specializations (pg. 280) | |
| 18·3 The lw Structure (pg. 282) | |
| 18·4 Rewriting Calls to Meta-functions (pg. 290) | |
| 18·5 Rewriting PLT Scheme Code (pg. 292) | |
| A. Appendix (pg. 297) | |
| A·1 Getting Started (pg. 297) | |
| A·2 Editing: Tips & Tricks (pg. 300) | |
| A·3 Running Programs: Tips & Tricks (pg. 303) | |
| A·4 Modules, Libraries, and Documentation (pg. 304) | |
| Part III. Applications (pg. 307) | |
| Chapter 19. Modular ACL2 (pg. 311) | |
| 19·1 ACL2 and Programming in the Large (pg. 311) | |
| 19·2 Design of Modular ACL2 (pg. 314) | |
| 19·3 Modeling Modular ACL2 (pg. 317) | |
| 19·4 Logical Meaning of Modules (pg. 318) | |
| 19·5 Executable Semantics of Programs (pg. 321) | |
| 19·6 Summary and Evaluation (pg. 322) | |
| 19·7 Developing with PLT Redex (pg. 325) | |
| Chapter 20. Modeling Scheme Macros (pg. 327) | |
| 20·1 Hygienic Macros (pg. 328) | |
| 20·2 Calculus (pg. 334) | |
| 20·3 Parsing Scheme without Macros (pg. 337) | |
| 20·4 The Core Macro Expander (pg. 344) | |
| 20·5 Outlook (pg. 354) | |
| Chapter 21. A Model of Java/Scheme Interoperability (pg. 357) | |
| 21·1 Java—Scheme Interoperability (pg. 357) | |
| 21·2 Background on Java + dynamic (pg. 358) | |
| 21·3 Modeling Interoperability (pg. 359) | |
| 21·4 The Language (pg. 360) | |
| 21·5 Adding Type Annotations (pg. 363) | |
| 21·6 Evaluation (pg. 371) | |
| 21·7 Related Work (pg. 379) | |
| 21·8 Conclusions and Supporting More Java Features (pg. 380) | |
| Chapter 22. Implementing Hidden Type Variables in Fortress (pg. 381) | |
| 22·1 Hidden Type Variables (pg. 381) | |
| 22·2 Applications of Hidden Type Variables (pg. 384) | |
| 22·3 Challenges When Implementing Hidden Type Variables (pg. 387) | |
| 22·4 Selecting Witnesses for Hidden Type Variables (pg. 388) | |
| 22·5 Annotating Programs with Witnesses (pg. 390) | |
| 22·6 A Redex Model for Hidden Type Variables (pg. 391) | |
| 22·7 Type Checking HTV1 (pg. 395) | |
| 22·8 Testing with PLT Redex (pg. 397) | |
| 22·9 Conclusion (pg. 399) | |
| 22·10 Implementation of Constraint Solving Algorithm (pg. 400) | |
| 22·11 Implementation of Type Hierarchy Traversal Algorithm (pg. 401) | |
| Chapter 23. Type Checking and Inference via Reductions (pg. 403) | |
| 23·1 Introduction (pg. 403) | |
| 23·2 Notation (pg. 403) | |
| 23·3 A Simple Type Checker (pg. 404) | |
| 23·4 System F (pg. 408) | |
| 23·5 Adding Nondeterministic Inference (pg. 409) | |
| 23·6 Unification-Based Inference (pg. 411) | |
| 23·7 Let-Bound Polymorphism (pg. 414) | |
| Chapter 24. Topsl (pg. 429) | |
| 24·1 Introduction (pg. 429) | |
| 24·2 Web Surveys (pg. 431) | |
| 24·3 Base Topsl (pg. 437) | |
| 24·4 Imperative Topsl (pg. 440) | |
| 24·5 Topsl + Scheme (pg. 442) | |
| 24·6 Web Topsl (pg. 448) | |
| 24·7 User + Core Topsl (pg. 452) | |
| 24·8 Using PLT Redex (pg. 454) | |
| 24·9 Implementation (pg. 455) | |
| 24·10 Related Work (pg. 456) | |
| 24·11 Conclusions (pg. 457) | |
| Chapter 25. Prototyping Nested Schedulers (pg. 459) | |
| 25·1 Introduction (pg. 459) | |
| 25·2 Our Scheduling Framework (pg. 461) | |
| 25·3 Formal Semantics (pg. 466) | |
| 25·4 Scheduler Utility Functions (pg. 474) | |
| 25·5 Scheduling Data-parallel Fibers (pg. 475) | |
| 25·6 Engines (pg. 476) | |
| 25·7 Prototyping in PLT Redex (pg. 481) | |
| 25·8 Conclusions (pg. 482) | |
| Bibliography (pg. 485) | |
| Index (pg. 495) | |
| Contents (pg. vii) | |
| Preface (pg. ix) | |
| Organization (pg. ix) | |
| To the Instructor (pg. x) | |
| To the Student (pg. x) | |
| Software (pg. xi) | |
| Acknowledgments (pg. xi) | |
| Part I. Reduction Semantics (pg. 1) | |
| Chapter 1. Semantics via Syntax (pg. 5) | |
| 1·1 Defining Sets. (pg. 5) | |
| 1·2 Relations (pg. 7) | |
| 1·3 Semantics as an Equivalence Relation (pg. 8) | |
| 1·4 Semantics via Reduction (pg. 9) | |
| 1·5 Reduction in Context (pg. 10) | |
| 1·6 Evaluation Functions (pg. 11) | |
| 1·7 Notation Summary (pg. 12) | |
| Chapter 2. Analyzing Syntactic Semantics (pg. 13) | |
| 2·1 From Questions to Mathematical Claims (pg. 13) | |
| 2·2 Answers as Theorems (pg. 14) | |
| Chapter 3. The λ-Calculus (pg. 23) | |
| 3·1 Functions and the λ-Calculus (pg. 23) | |
| 3·2 λ-Calculus: Syntax and Reductions (pg. 25) | |
| 3·3 Encoding Booleans (pg. 29) | |
| 3·4 Encoding Pairs (pg. 30) | |
| 3·5 Encoding Numbers (pg. 31) | |
| 3·6 Encodings and Errors (pg. 33) | |
| 3·7 Recursion (pg. 34) | |
| 3·8 Consistency and Normal Forms (pg. 38) | |
| 3·9 Normal Forms and Reduction Strategies (pg. 40) | |
| 3·10 History (pg. 43) | |
| Chapter 4. ISWIM (pg. 45) | |
| 4·1 ISWIM Expressions (pg. 45) | |
| 4·2 Calculating with ISWIM (pg. 47) | |
| 4·3 Alpha, Eta, and Quotients (pg. 49) | |
| 4·4 The Yv Combinator (pg. 50) | |
| 4·5 Evaluation (pg. 52) | |
| 4·6 Consistency (pg. 52) | |
| 4·7 Observational Equivalence (pg. 58) | |
| 4·8 History (pg. 63) | |
| Chapter 5. An Abstract Syntax Machine (pg. 65) | |
| 5·1 Standard Reductions (pg. 65) | |
| 5·2 The Standard Reduction Theorem (pg. 69) | |
| 5·3 Reasoning about Observational Equivalence (pg. 80) | |
| 5·4 Uniform Evaluation (pg. 84) | |
| 5·5 History (pg. 87) | |
| Chapter 6. Abstract Register Machines (pg. 89) | |
| 6·1 The CC Machine (pg. 89) | |
| 6·2 The SCC Machine (pg. 94) | |
| 6·3 The CK Machine (pg. 99) | |
| 6·4 The CEK Machine (pg. 100) | |
| 6·5 History (pg. 105) | |
| Chapter 7. Tail Calls and More Space Savings (pg. 107) | |
| 7·1 SECD Machine (pg. 107) | |
| 7·2 Space for Evaluation Contexts (pg. 109) | |
| 7·3 Space for Environments (pg. 112) | |
| 7·4 History (pg. 114) | |
| Chapter 8. Control (pg. 115) | |
| 8·1 Error ISWIM (pg. 116) | |
| 8·2 Relating ISWIM and Error ISWIM (pg. 124) | |
| 8·3 Handler ISWIM (pg. 129) | |
| 8·4 Continuation ISWIM and Total Control (pg. 139) | |
| 8·5 History (pg. 144) | |
| Chapter 9. State (pg. 145) | |
| 9·1 Programming in State ISWIM (pg. 146) | |
| 9·2 An Evaluator for State ISWIM (pg. 148) | |
| 9·3 The State ISWIM Calculus (pg. 154) | |
| 9·4 The CESK Machine (pg. 165) | |
| 9·5 Space and Garbage Collection (pg. 167) | |
| 9·6 History (pg. 173) | |
| Chapter 10. Simply Typed ISWIM (pg. 175) | |
| 10·1 Simply Typed ISWIM (pg. 176) | |
| 10·2 Typed Programs Don’t Go Wrong (pg. 186) | |
| 10·3 Types and Recursion (pg. 190) | |
| 10·4 Typed Programs Go to Specific Stuck States (pg. 197) | |
| 10·5 History (pg. 198) | |
| Part II. PLT Redex (pg. 201) | |
| Chapter 11. The Basics (pg. 205) | |
| 11·1 PLT Redex and PLT Scheme (pg. 205) | |
| 11·2 Specifying Abstract Syntax (pg. 207) | |
| 11·3 Specifying Reduction Relations (pg. 210) | |
| 11·4 Tracing (pg. 212) | |
| 11·5 Variation on a Theme (pg. 213) | |
| Chapter 12. Variables and Meta-functions (pg. 217) | |
| 12·1 More on Redex Grammars (pg. 217) | |
| 12·2 Meta-functions (pg. 219) | |
| 12·3 Reductions via with Clauses (pg. 224) | |
| Chapter 13. Layered Development (pg. 227) | |
| 13·1 Extending Languages (pg. 227) | |
| 13·2 Extending Reduction Relations (pg. 230) | |
| 13·3 Side Conditions (pg. 234) | |
| Chapter 14. Testing (pg. 237) | |
| 14·1 Test Cases, Test Suites (pg. 237) | |
| 14·2 Abstracting over Test Cases (pg. 238) | |
| 14·3 Testing Properties (pg. 240) | |
| 14·4 The CK Machine (pg. 241) | |
| Chapter 15. Debugging (pg. 245) | |
| 15·1 Visual Debugging, Take 1 (pg. 245) | |
| 15·2 Type Checking, Take 1 (pg. 248) | |
| 15·3 Visual Debugging, Take 2 (pg. 253) | |
| 15·4 Type Checking, Take 2 (pg. 256) | |
| Chapter 16. Case Study 1 (pg. 259) | |
| 16·1 Adding Mutation (pg. 259) | |
| 16·2 Evaluation Everywhere (pg. 261) | |
| 16·3 R6RS: A First Attempt (pg. 263) | |
| 16·4 R6RS: A Second Attempt (pg. 266) | |
| 16·5 R6RS: Finally (pg. 268) | |
| Chapter 17. Case Study 2 (pg. 271) | |
| 17·1 Continuations as Functions (pg. 271) | |
| 17·2 Continuations as Evaluation Contexts (pg. 273) | |
| Chapter 18. Typesetting (pg. 277) | |
| 18·1 The Defaults (pg. 277) | |
| 18·2 Simple Specializations (pg. 280) | |
| 18·3 The lw Structure (pg. 282) | |
| 18·4 Rewriting Calls to Meta-functions (pg. 290) | |
| 18·5 Rewriting PLT Scheme Code (pg. 292) | |
| A. Appendix (pg. 297) | |
| A·1 Getting Started (pg. 297) | |
| A·2 Editing: Tips & Tricks (pg. 300) | |
| A·3 Running Programs: Tips & Tricks (pg. 303) | |
| A·4 Modules, Libraries, and Documentation (pg. 304) | |
| Part III. Applications (pg. 307) | |
| Chapter 19. Modular ACL2 (pg. 311) | |
| 19·1 ACL2 and Programming in the Large (pg. 311) | |
| 19·2 Design of Modular ACL2 (pg. 314) | |
| 19·3 Modeling Modular ACL2 (pg. 317) | |
| 19·4 Logical Meaning of Modules (pg. 318) | |
| 19·5 Executable Semantics of Programs (pg. 321) | |
| 19·6 Summary and Evaluation (pg. 322) | |
| 19·7 Developing with PLT Redex (pg. 325) | |
| Chapter 20. Modeling Scheme Macros (pg. 327) | |
| 20·1 Hygienic Macros (pg. 328) | |
| 20·2 Calculus (pg. 334) | |
| 20·3 Parsing Scheme without Macros (pg. 337) | |
| 20·4 The Core Macro Expander (pg. 344) | |
| 20·5 Outlook (pg. 354) | |
| Chapter 21. A Model of Java/Scheme Interoperability (pg. 357) | |
| 21·1 Java—Scheme Interoperability (pg. 357) | |
| 21·2 Background on Java + dynamic (pg. 358) | |
| 21·3 Modeling Interoperability (pg. 359) | |
| 21·4 The Language (pg. 360) | |
| 21·5 Adding Type Annotations (pg. 363) | |
| 21·6 Evaluation (pg. 371) | |
| 21·7 Related Work (pg. 379) | |
| 21·8 Conclusions and Supporting More Java Features (pg. 380) | |
| Chapter 22. Implementing Hidden Type Variables in Fortress (pg. 381) | |
| 22·1 Hidden Type Variables (pg. 381) | |
| 22·2 Applications of Hidden Type Variables (pg. 384) | |
| 22·3 Challenges When Implementing Hidden Type Variables (pg. 387) | |
| 22·4 Selecting Witnesses for Hidden Type Variables (pg. 388) | |
| 22·5 Annotating Programs with Witnesses (pg. 390) | |
| 22·6 A Redex Model for Hidden Type Variables (pg. 391) | |
| 22·7 Type Checking HTV1 (pg. 395) | |
| 22·8 Testing with PLT Redex (pg. 397) | |
| 22·9 Conclusion (pg. 399) | |
| 22·10 Implementation of Constraint Solving Algorithm (pg. 400) | |
| 22·11 Implementation of Type Hierarchy Traversal Algorithm (pg. 401) | |
| Chapter 23. Type Checking and Inference via Reductions (pg. 403) | |
| 23·1 Introduction (pg. 403) | |
| 23·2 Notation (pg. 403) | |
| 23·3 A Simple Type Checker (pg. 404) | |
| 23·4 System F (pg. 408) | |
| 23·5 Adding Nondeterministic Inference (pg. 409) | |
| 23·6 Unification-Based Inference (pg. 411) | |
| 23·7 Let-Bound Polymorphism (pg. 414) | |
| Chapter 24. Topsl (pg. 429) | |
| 24·1 Introduction (pg. 429) | |
| 24·2 Web Surveys (pg. 431) | |
| 24·3 Base Topsl (pg. 437) | |
| 24·4 Imperative Topsl (pg. 440) | |
| 24·5 Topsl + Scheme (pg. 442) | |
| 24·6 Web Topsl (pg. 448) | |
| 24·7 User + Core Topsl (pg. 452) | |
| 24·8 Using PLT Redex (pg. 454) | |
| 24·9 Implementation (pg. 455) | |
| 24·10 Related Work (pg. 456) | |
| 24·11 Conclusions (pg. 457) | |
| Chapter 25. Prototyping Nested Schedulers (pg. 459) | |
| 25·1 Introduction (pg. 459) | |
| 25·2 Our Scheduling Framework (pg. 461) | |
| 25·3 Formal Semantics (pg. 466) | |
| 25·4 Scheduler Utility Functions (pg. 474) | |
| 25·5 Scheduling Data-parallel Fibers (pg. 475) | |
| 25·6 Engines (pg. 476) | |
| 25·7 Prototyping in PLT Redex (pg. 481) | |
| 25·8 Conclusions (pg. 482) | |
| Bibliography (pg. 485) | |
| Index (pg. 495) | |
| Contents (pg. vii) | |
| Preface (pg. ix) | |
| Organization (pg. ix) | |
| To the Instructor (pg. x) | |
| To the Student (pg. x) | |
| Software (pg. xi) | |
| Acknowledgments (pg. xi) | |
| Part I. Reduction Semantics (pg. 1) | |
| Chapter 1. Semantics via Syntax (pg. 5) | |
| 1·1 Defining Sets. (pg. 5) | |
| 1·2 Relations (pg. 7) | |
| 1·3 Semantics as an Equivalence Relation (pg. 8) | |
| 1·4 Semantics via Reduction (pg. 9) | |
| 1·5 Reduction in Context (pg. 10) | |
| 1·6 Evaluation Functions (pg. 11) | |
| 1·7 Notation Summary (pg. 12) | |
| Chapter 2. Analyzing Syntactic Semantics (pg. 13) | |
| 2·1 From Questions to Mathematical Claims (pg. 13) | |
| 2·2 Answers as Theorems (pg. 14) | |
| Chapter 3. The λ-Calculus (pg. 23) | |
| 3·1 Functions and the λ-Calculus (pg. 23) | |
| 3·2 λ-Calculus: Syntax and Reductions (pg. 25) | |
| 3·3 Encoding Booleans (pg. 29) | |
| 3·4 Encoding Pairs (pg. 30) | |
| 3·5 Encoding Numbers (pg. 31) | |
| 3·6 Encodings and Errors (pg. 33) | |
| 3·7 Recursion (pg. 34) | |
| 3·8 Consistency and Normal Forms (pg. 38) | |
| 3·9 Normal Forms and Reduction Strategies (pg. 40) | |
| 3·10 History (pg. 43) | |
| Chapter 4. ISWIM (pg. 45) | |
| 4·1 ISWIM Expressions (pg. 45) | |
| 4·2 Calculating with ISWIM (pg. 47) | |
| 4·3 Alpha, Eta, and Quotients (pg. 49) | |
| 4·4 The Yv Combinator (pg. 50) | |
| 4·5 Evaluation (pg. 52) | |
| 4·6 Consistency (pg. 52) | |
| 4·7 Observational Equivalence (pg. 58) | |
| 4·8 History (pg. 63) | |
| Chapter 5. An Abstract Syntax Machine (pg. 65) | |
| 5·1 Standard Reductions (pg. 65) | |
| 5·2 The Standard Reduction Theorem (pg. 69) | |
| 5·3 Reasoning about Observational Equivalence (pg. 80) | |
| 5·4 Uniform Evaluation (pg. 84) | |
| 5·5 History (pg. 87) | |
| Chapter 6. Abstract Register Machines (pg. 89) | |
| 6·1 The CC Machine (pg. 89) | |
| 6·2 The SCC Machine (pg. 94) | |
| 6·3 The CK Machine (pg. 99) | |
| 6·4 The CEK Machine (pg. 100) | |
| 6·5 History (pg. 105) | |
| Chapter 7. Tail Calls and More Space Savings (pg. 107) | |
| 7·1 SECD Machine (pg. 107) | |
| 7·2 Space for Evaluation Contexts (pg. 109) | |
| 7·3 Space for Environments (pg. 112) | |
| 7·4 History (pg. 114) | |
| Chapter 8. Control (pg. 115) | |
| 8·1 Error ISWIM (pg. 116) | |
| 8·2 Relating ISWIM and Error ISWIM (pg. 124) | |
| 8·3 Handler ISWIM (pg. 129) | |
| 8·4 Continuation ISWIM and Total Control (pg. 139) | |
| 8·5 History (pg. 144) | |
| Chapter 9. State (pg. 145) | |
| 9·1 Programming in State ISWIM (pg. 146) | |
| 9·2 An Evaluator for State ISWIM (pg. 148) | |
| 9·3 The State ISWIM Calculus (pg. 154) | |
| 9·4 The CESK Machine (pg. 165) | |
| 9·5 Space and Garbage Collection (pg. 167) | |
| 9·6 History (pg. 173) | |
| Chapter 10. Simply Typed ISWIM (pg. 175) | |
| 10·1 Simply Typed ISWIM (pg. 176) | |
| 10·2 Typed Programs Don’t Go Wrong (pg. 186) | |
| 10·3 Types and Recursion (pg. 190) | |
| 10·4 Typed Programs Go to Specific Stuck States (pg. 197) | |
| 10·5 History (pg. 198) | |
| Part II. PLT Redex (pg. 201) | |
| Chapter 11. The Basics (pg. 205) | |
| 11·1 PLT Redex and PLT Scheme (pg. 205) | |
| 11·2 Specifying Abstract Syntax (pg. 207) | |
| 11·3 Specifying Reduction Relations (pg. 210) | |
| 11·4 Tracing (pg. 212) | |
| 11·5 Variation on a Theme (pg. 213) | |
| Chapter 12. Variables and Meta-functions (pg. 217) | |
| 12·1 More on Redex Grammars (pg. 217) | |
| 12·2 Meta-functions (pg. 219) | |
| 12·3 Reductions via with Clauses (pg. 224) | |
| Chapter 13. Layered Development (pg. 227) | |
| 13·1 Extending Languages (pg. 227) | |
| 13·2 Extending Reduction Relations (pg. 230) | |
| 13·3 Side Conditions (pg. 234) | |
| Chapter 14. Testing (pg. 237) | |
| 14·1 Test Cases, Test Suites (pg. 237) | |
| 14·2 Abstracting over Test Cases (pg. 238) | |
| 14·3 Testing Properties (pg. 240) | |
| 14·4 The CK Machine (pg. 241) | |
| Chapter 15. Debugging (pg. 245) | |
| 15·1 Visual Debugging, Take 1 (pg. 245) | |
| 15·2 Type Checking, Take 1 (pg. 248) | |
| 15·3 Visual Debugging, Take 2 (pg. 253) | |
| 15·4 Type Checking, Take 2 (pg. 256) | |
| Chapter 16. Case Study 1 (pg. 259) | |
| 16·1 Adding Mutation (pg. 259) | |
| 16·2 Evaluation Everywhere (pg. 261) | |
| 16·3 R6RS: A First Attempt (pg. 263) | |
| 16·4 R6RS: A Second Attempt (pg. 266) | |
| 16·5 R6RS: Finally (pg. 268) | |
| Chapter 17. Case Study 2 (pg. 271) | |
| 17·1 Continuations as Functions (pg. 271) | |
| 17·2 Continuations as Evaluation Contexts (pg. 273) | |
| Chapter 18. Typesetting (pg. 277) | |
| 18·1 The Defaults (pg. 277) | |
| 18·2 Simple Specializations (pg. 280) | |
| 18·3 The lw Structure (pg. 282) | |
| 18·4 Rewriting Calls to Meta-functions (pg. 290) | |
| 18·5 Rewriting PLT Scheme Code (pg. 292) | |
| A. Appendix (pg. 297) | |
| A·1 Getting Started (pg. 297) | |
| A·2 Editing: Tips & Tricks (pg. 300) | |
| A·3 Running Programs: Tips & Tricks (pg. 303) | |
| A·4 Modules, Libraries, and Documentation (pg. 304) | |
| Part III. Applications (pg. 307) | |
| Chapter 19. Modular ACL2 (pg. 311) | |
| 19·1 ACL2 and Programming in the Large (pg. 311) | |
| 19·2 Design of Modular ACL2 (pg. 314) | |
| 19·3 Modeling Modular ACL2 (pg. 317) | |
| 19·4 Logical Meaning of Modules (pg. 318) | |
| 19·5 Executable Semantics of Programs (pg. 321) | |
| 19·6 Summary and Evaluation (pg. 322) | |
| 19·7 Developing with PLT Redex (pg. 325) | |
| Chapter 20. Modeling Scheme Macros (pg. 327) | |
| 20·1 Hygienic Macros (pg. 328) | |
| 20·2 Calculus (pg. 334) | |
| 20·3 Parsing Scheme without Macros (pg. 337) | |
| 20·4 The Core Macro Expander (pg. 344) | |
| 20·5 Outlook (pg. 354) | |
| Chapter 21. A Model of Java/Scheme Interoperability (pg. 357) | |
| 21·1 Java—Scheme Interoperability (pg. 357) | |
| 21·2 Background on Java + dynamic (pg. 358) | |
| 21·3 Modeling Interoperability (pg. 359) | |
| 21·4 The Language (pg. 360) | |
| 21·5 Adding Type Annotations (pg. 363) | |
| 21·6 Evaluation (pg. 371) | |
| 21·7 Related Work (pg. 379) | |
| 21·8 Conclusions and Supporting More Java Features (pg. 380) | |
| Chapter 22. Implementing Hidden Type Variables in Fortress (pg. 381) | |
| 22·1 Hidden Type Variables (pg. 381) | |
| 22·2 Applications of Hidden Type Variables (pg. 384) | |
| 22·3 Challenges When Implementing Hidden Type Variables (pg. 387) | |
| 22·4 Selecting Witnesses for Hidden Type Variables (pg. 388) | |
| 22·5 Annotating Programs with Witnesses (pg. 390) | |
| 22·6 A Redex Model for Hidden Type Variables (pg. 391) | |
| 22·7 Type Checking HTV1 (pg. 395) | |
| 22·8 Testing with PLT Redex (pg. 397) | |
| 22·9 Conclusion (pg. 399) | |
| 22·10 Implementation of Constraint Solving Algorithm (pg. 400) | |
| 22·11 Implementation of Type Hierarchy Traversal Algorithm (pg. 401) | |
| Chapter 23. Type Checking and Inference via Reductions (pg. 403) | |
| 23·1 Introduction (pg. 403) | |
| 23·2 Notation (pg. 403) | |
| 23·3 A Simple Type Checker (pg. 404) | |
| 23·4 System F (pg. 408) | |
| 23·5 Adding Nondeterministic Inference (pg. 409) | |
| 23·6 Unification-Based Inference (pg. 411) | |
| 23·7 Let-Bound Polymorphism (pg. 414) | |
| Chapter 24. Topsl (pg. 429) | |
| 24·1 Introduction (pg. 429) | |
| 24·2 Web Surveys (pg. 431) | |
| 24·3 Base Topsl (pg. 437) | |
| 24·4 Imperative Topsl (pg. 440) | |
| 24·5 Topsl + Scheme (pg. 442) | |
| 24·6 Web Topsl (pg. 448) | |
| 24·7 User + Core Topsl (pg. 452) | |
| 24·8 Using PLT Redex (pg. 454) | |
| 24·9 Implementation (pg. 455) | |
| 24·10 Related Work (pg. 456) | |
| 24·11 Conclusions (pg. 457) | |
| Chapter 25. Prototyping Nested Schedulers (pg. 459) | |
| 25·1 Introduction (pg. 459) | |
| 25·2 Our Scheduling Framework (pg. 461) | |
| 25·3 Formal Semantics (pg. 466) | |
| 25·4 Scheduler Utility Functions (pg. 474) | |
| 25·5 Scheduling Data-parallel Fibers (pg. 475) | |
| 25·6 Engines (pg. 476) | |
| 25·7 Prototyping in PLT Redex (pg. 481) | |
| 25·8 Conclusions (pg. 482) | |
| Bibliography (pg. 485) | |
| Index (pg. 495) | |
Matthias Felleisen
Matthias Felleisen is Trustee Professor of Computer Science at Northeastern University, recipient of the Karl V. Karlstrom Outstanding Educator Award, and co-author (with Daniel Friedman) of The Little Schemer and three other "Little" books published by the MIT Press.
Matthew Flatt
Matthew Flatt is Associate Professor in the School of Computing at the University of Utah.
Robert Bruce Findler
Robert Bruce Findler is an Associate Professor of Computer Science at Northwestern University.
|
eTextbook
Go paperless today! Available online anytime, nothing to download or install.
Features
|
