TY  - BOOK
AU  - Harper, Robert
TI  - Practical foundations for programming language
SN  - 9781107029576
AV  - QA 76.7 .H37 2013  
PY  - 2013///
CY  - Cambridge
PB  - Cambridge University Press
KW  - PROGRAMMING LANGUAGES (ELECTRONIC COMPUTERS)
N1  - Includes bibliographical references; Cover; Practical Foundations for Programming Languages; Title; Copyright; Contents; Preface; PART I: Judgments and Rules; 1 Syntactic Objects; 1.1 Abstract Syntax Trees; 1.2 Abstract Binding Trees; 1.3 Notes; 2 Inductive Definitions; 2.1 Judgments; 2.2 Inference Rules; 2.3 Derivations; 2.4 Rule Induction; 2.5 Iterated and Simultaneous Inductive Definitions; 2.6 Defining Functions by Rules; 2.7 Modes; 2.8 Notes; 3 Hypothetical and General Judgments; 3.1 Hypothetical Judgments; 3.1.1 Derivability; 3.1.2 Admissibility; 3.2 Hypothetical Inductive Definitions; 3.3 General Judgments.  3.4 Generic Inductive Definitions3.5 Notes; PART II: Statics and Dynamics; 4 Statics; 4.1 Syntax; 4.2 Type System; 4.3 Structural Properties; 4.4 Notes; 5 Dynamics; 5.1 Transition Systems; 5.2 Structural Dynamics; 5.3 Contextual Dynamics; 5.4 Equational Dynamics; 5.5 Notes; 6 Type Safety; 6.1 Preservation; 6.2 Progress; 6.3 Run-Time Errors; 6.4 Notes; 7 Evaluation Dynamics; 7.1 Evaluation Dynamics; 7.2 Relating Structural and Evaluation Dynamics; 7.3 Type Safety, Revisited; 7.4 Cost Dynamics; 7.5 Notes; PART III: Function Types; 8 Function Definitions and Values; 8.1 First-Order Functions.  8.2 Higher-Order Functions8.3 Evaluation Dynamics and Definitional Equality; 8.4 Dynamic Scope; 8.5 Notes; 9 Godel's T; 9.1 Statics; 9.2 Dynamics; 9.3 Definability; 9.4 Undefinability; 9.5 Notes; 10 Plotkin's PCF; 10.1 Statics; 10.2 Dynamics; 10.3 Definability; 10.4 Notes; PART IV: Finite Data Types; 11 Product Types; 11.1 Nullary and Binary Products; 11.2 Finite Products; 11.3 Primitive and Mutual Recursions; 11.4 Notes; 12 Sum Types; 12.1 Nullary and Binary Sums; 12.2 Finite Sums; 12.3 Applications of Sum Types; 12.3.1 Void and Unit; 12.3.2 Booleans; 12.3.3 Enumerations; 12.3.4 Options.  12.4 Notes13 Pattern Matching; 13.1 A Pattern Language; 13.2 Statics; 13.3 Dynamics; 13.4 Exhaustiveness and Redundancy; 13.4.1 Match Constraints; 13.4.2 Enforcing Exhaustiveness and Redundancy; 13.4.3 Checking Exhaustiveness and Redundancy; 13.5 Notes; 14 Generic Programming; 14.1 Introduction; 14.2 Type Operators; 14.3 Generic Extension; 14.4 Notes; PART V: Infinite Data Types; 15 Inductive and Coinductive Types; 15.1 Motivating Examples; 15.2 Statics; 15.2.1 Types; 15.2.2 Expressions; 15.3 Dynamics; 15.4 Notes; 16 Recursive Types; 16.1 Solving Type Isomorphisms.  16.2 Recursive Data Structures16.3 Self-Reference; 16.4 The Origin of State; 16.5 Notes; PART VI: Dynamic Types; 17 The Untyped -Calculus; 17.1 The -Calculus; 17.2 Definability; 17.3 Scott's Theorem; 17.4 Untyped Means Unityped; 17.5 Notes; 18 Dynamic Typing; 18.1 Dynamically Typed PCF; 18.2 Variations and Extensions; 18.3 Critique of Dynamic Typing; 18.4 Notes; 19 Hybrid Typing; 19.1 A Hybrid Language; 19.2 Dynamics as Static Typing; 19.3 Optimization of Dynamic Typing; 19.4 Static Versus Dynamic Typing; 19.5 Notes; PART VII: Variable Types; 20 Girard's System F; 20.1 System F.  Part I. Judgments and rules ; Syntactic objects -- Inductive definitions -- Hypothetical and general judgments -- Part II. Statics and dynamics ; Statics -- Dynamics -- Type safety -- Evaluation dynamics -- Part III. Function types ; Function definitions and values -- G├╢del's T -- Plotkin's PCF -- Part IV. Finite data types ; Product types -- Sum types -- Pattern matching -- Generic programming -- Part V. Infinite data types ; Inductive and coinductive types -- Recursive types -- Part VI. Dynamic types ; The untyped ╬╗-calculus -- Dynamic typing -- Hybrid typing -- Part VII. Variable types ; Girard's System F -- Abstract types -- Constructors and kinds -- Part VIII. Subtyping ; Subtyping -- Singleton kinds -- Part IX. Classes and methods ; Dynamic dispatch -- Inheritance -- Part X. Exceptions and continuations ; Control stacks -- Exceptions -- Continuations -- Part XI. Types and propositions ; Constructive logic -- Classical logic -- Part XII. Symbols ; Symbols -- Fluid binding -- Dynamic classification -- Part XIII. State ; Modernized Algol -- Assignable references -- Part XIV. Laziness ; Lazy evaluation -- Polarization -- Part XV. Parallelism ; Nested parallelism -- Futures and speculations -- Part XVI. Concurrency ; Process calculus -- Concurrent Algol -- Distributed Algol -- Part XVII. Modularity ; Components and linking -- Type abstractions and type classes -- Hierarchy and parameterization -- Part XVIII. Equational reasoning ; Equational reasoning for T -- Equational reasoning for PCF -- Parametricity -- Process equivalence -- Part XIX. Appendix ; Finite sets and finite functions
N2  - This book offers a fresh perspective on the fundamentals of programming languages through the use of type theory
ER  -