Practical foundations for programming languages

Practical foundations for programming languages / Robert Harper.

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 inste...

Full description

Saved in:
Bibliographic Details
Main Author: Harper, Robert, 1957-
Format: eBook
Language:English
Published: Cambridge, UK ; New York : Cambridge University Press, 2013.
Subjects:
Programming languages (Electronic computers)
Programming languages (Electronic computers) > Syntax.
Programming languages (Electronic computers) > Semantics.
COMPUTERS > Programming Languages > General.
Programming languages (Electronic computers) > Syntax
Programming languages (Electronic computers) > Semantics
Programmiersprache
Online Access:Click for online access
Table of Contents:
  • 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.

Similar Items