Book contents
- Frontmatter
- Contents
- Preface to the Second Edition
- Preface to the First Edition
- Part I Judgments and Rules
- Part II Statics and Dynamics
- Part III Total Functions
- Part IV Finite Data Types
- Part V Types and Propositions
- Part VI Infinite Data Types
- Part VII Variable Types
- Part VIII Partiality and Recursive Types
- Part IX Dynamic Types
- Part X Subtyping
- Part XI Dynamic Dispatch
- Part XII Control Flow
- Part XIII Symbolic Data
- Part XIV Mutable State
- Part XV Parallelism
- Part XVI Concurrency and Distribution
- Part XVII Modularity
- Part XVIII Equational Reasoning
- Part XIX Appendices
- References
- Index
Preface to the Second Edition
Published online by Cambridge University Press: 05 March 2016
- Frontmatter
- Contents
- Preface to the Second Edition
- Preface to the First Edition
- Part I Judgments and Rules
- Part II Statics and Dynamics
- Part III Total Functions
- Part IV Finite Data Types
- Part V Types and Propositions
- Part VI Infinite Data Types
- Part VII Variable Types
- Part VIII Partiality and Recursive Types
- Part IX Dynamic Types
- Part X Subtyping
- Part XI Dynamic Dispatch
- Part XII Control Flow
- Part XIII Symbolic Data
- Part XIV Mutable State
- Part XV Parallelism
- Part XVI Concurrency and Distribution
- Part XVII Modularity
- Part XVIII Equational Reasoning
- Part XIX Appendices
- References
- Index
Summary
Writing the second edition to a textbook incurs the same risk as building the second version of a software system. It is difficult to make substantive improvements, while avoiding the temptation to overburden and undermine the foundation on which one is building.With the hope of avoiding the second system effect, I have sought to make corrections, revisions, expansions, and deletions that improve the coherence of the development, remove some topics that distract from the main themes, add new topics that were omitted from the first edition, and include exercises for almost every chapter.
The revision removes a number of typographical errors, corrects a few material errors (especially the formulation of the parallel abstract machine and of concurrency in Algol), and improves the writing throughout. Some chapters have been deleted (general pattern matching and polarization, restricted forms of polymorphism), some have been completely rewritten (the chapter on higher kinds), some have been substantially revised (general and parametric inductive definitions, concurrent and distributed Algol), several have been reorganized (to better distinguish partial from total type theories), and a new chapter has been added (on type refinements). Titular attributions on several chapters have been removed, not to diminish credit, but to avoid confusion between the present and the original formulations of several topics. A new system of (pronounceable!) language names has been introduced throughout. The exercises generally seek to expand on the ideas in the main text, and their solutions often involve significant technical ideas that merit study. Routine exercises of the kind one might include in a homework assignment are deliberately few.
My purpose in writing this book is to establish a comprehensive framework for formulating and analyzing a broad range of ideas in programming languages. If language design and programming methodology are to advance from a trade-craft to a rigorous discipline, it is essential that we first get the definitions right. Then, and only then, can there be meaningful analysis and consolidation of ideas. My hope is that I have helped to build such a foundation.
I am grateful to Stephen Brookes, Evan Cavallo, Karl Crary, Jon Sterling, James R. Wilcox and Todd Wilson for their help in critiquing drafts of this edition and for their suggestions for modification and revision. I thank my department head, Frank Pfenning, for his support ofmy work on the completion of this edition.
- Type
- Chapter
- Information
- Practical Foundations for Programming Languages , pp. xv - xviPublisher: Cambridge University PressPrint publication year: 2016