Practical foundations for programming language /
Robert Harper.
- New York : Cambridge University Press, c2013
- xviii, 471 pages : illustrations ; 26 cm
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.
Types are the central organizing principle of the theory of programming languages. In this innovative book, Professor Robert Harper offers a fresh perspective on the fundamentals of these languages through the use of type theory. Whereas most textbooks on the subject emphasize taxonomy, Harper instead emphasizes genetics, examining the building blocks from which all programming languages are constructed. Language features are manifestations of type structure. The syntax of a language is governed by the constructs that define its types, and its semantics is determined by the interactions among those constructs. The soundness of a language design - the absence of ill-defined programs - follows naturally. Professor Harper's presentation is simultaneously rigorous and intuitive, relying on elementary mathematics. The framework he outlines scales easily to a rich variety of language concepts and is directly applicable to their implementation. The result is a lucid introduction to programming theory that is both accessible and practical.--Publisher.