This text develops a comprehensive theory of programming languages based on type systems and structural operational semantics. Language concepts are precisely defined by their static and dynamic semantics, presenting the essential tools both intuitively and rigorously while relying on only elementary mathematics. These tools are used to analyze and prove properties of languages and provide the framework for combining and comparing language features. The broad range of concepts includes fundamental data types such as sums and products, polymorphic and abstract types, dynamic typing, dynamic dispatch, subtyping and refinement types, symbols and dynamic classification, parallelism and cost semantics, and concurrency and distribution. The methods are directly applicable to language implementation, to the development of logics for reasoning about programs, and to the formal verification language properties such as type safety. This thoroughly revised second edition includes exercises at the end of nearly every chapter and a new chapter on type refinements.

Table of Contents

Part I Judgments and Rules

1 Abstract Syntax

2 Inductive Definitions

3 Hypothetical and General Judgments

Part II Statics and Dynamics

4 Statics

5 Dynamics

6 Type Safety

7 Evaluation Dynamics

Part Ill Total Functions

8 Function Definitions and Values

9 System T of Higher-Order Recursion

Part IV Finite Data Types

10 Product Types

11 Sum Types

Part V Types and Propositions

12 Constructive Logic

13 Classical Logic

Part VI Infinite Data Types

14 Generic Programming

15 Inductive and Coinductive Types

Part VII Variable Types

16 System F of Polymorphic Types

17 Abstract Types

18 Higher Kinds

Part VIII Partiality and Recursive Types

19 System PCF of Recursive Functions

20 System FPC of Recursive Types

Part IX Dynamic Types

21 The Untyped 71-Calculus

22 Dynamic Typing

23 Hybrid Typing

Part X Subtyping

24 Structural Subtyping

25 Behavioral Typing

Part XI Dynamic Dispatch

26 Classes and Methods

27 Inheritance

Part XII Control Flow

28 Control Stacks

29 Exceptions

30 Continuations

Part XIII Symbolic Data

31 Symbols

32 Fluid Binding

33 Dynamic Classification

Part XIV Mutable State

34 Modernized Algol

35 Assignable References

36 Lazy Evaluation

Part XV Parallelism

37 Nested Parallelism

38 Futures and Speculations

Part XVI Concurrency and Distribution

39 Process Calculus

40 Concurrent Algol

41 Distributed Algol

Part XVII Modularity

42 Modularity and Linking

43 Singleton Kinds and Subkinding

44 Type Abstractions and Type Classes

45 Hierarchy and Parameterization

Part XVIII Equational Reasoning

46 Equality for System T

47 Equality for System PCF

48 Parametricity

49 Process Equivalence

Part XIX Appendices

A Background on Finite Sets

About the Author

Robert Harper is a professor in the Computer Science Department at Carnegie Mellon University. His main research interest is in the application of type theory to the design and implementation of programming languages and to the mechanization of their metatheory. Harper is a recipient of the Allen Newell Medal for Research Excellence and the Herbert A. Simon Award for Teaching Excellence, and is an Association for Computing Machinery Fellow.