Preface to the first edition Types are the central organizing principle of the theory of programming languages.Language fea- tures 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. The purpose of this book is to explain this remark.A variety of programming language features are analyzed in the unifying framework of type theory.A language feature is defined by its statics, the rules governing the use of the feature in a program,and its dynamics,the rules defining how programs using this feature are to be executed.The concept of safety emerges as the coherence of the statics and the dynamics of a language. In this way we establish a foundation for the study of programming languages.But why these particular methods?The main justification is provided by the book itself.The methods we use are both precise and intuitive,providing a uniform framework for explaining programming language concepts.Importantly,these methods scale to a wide range of programming language concepts, supporting rigorous analysis of their properties.Although it would require another book in itself to justify this assertion,these methods are also practical in that they are directly applicable to imple- mentation and uniquely effective as a basis for mechanized reasoning.No other framework offers as much Being a consolidation and distillation of decades of research,this book does not provide an exhaustive account of the history of the ideas that inform it.Suffice it to say that much of the de- velopment is not original,but rather is largely a reformulation of what has gone before.The notes at the end of each chapter signpost the major developments,but are not intended as a complete guide to the literature.For further information and alternative perspectives,the reader is referred to such excellent sources as Constable (1986),Constable(1998),Girard(1989),Martin-Lof(1984), Mitchell(1996),Pierce(2002,2004),and Reynolds(1998). The book is divided into parts that are,in the main,independent of one another.Parts I and II, however,provide the foundation for the rest of the book,and must therefore be considered prior to all other parts.On first reading it may be best to skim Part I,and begin in earnest with Part II, returning to Part I for clarification of the logical framework in which the rest of the book is cast. Numerous people have read and commented on earlier editions of this book,and have sug- gested corrections and improvements to it.I am particularly grateful to Umut Acar,Jesper Louis Andersen,Carlo Angiuli,Andrew Appel,Stephanie Balzer,Eric Bergstrom,Guy E.Blelloch,Il- iano Cervesato,Lin Chase,Karl Crary,Rowan Davies,Derek Dreyer,Dan Licata,Zhong Shao,PREVIEW Preface to the First Edition Types are the central organizing principle of the theory of programming languages. Language fea￾tures 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. The purpose of this book is to explain this remark. A variety of programming language features are analyzed in the unifying framework of type theory. A language feature is defined by its statics, the rules governing the use of the feature in a program, and its dynamics, the rules defining how programs using this feature are to be executed. The concept of safety emerges as the coherence of the statics and the dynamics of a language. In this way we establish a foundation for the study of programming languages. But why these particular methods? The main justification is provided by the book itself. The methods we use are both precise and intuitive, providing a uniform framework for explaining programming language concepts. Importantly, these methods scale to a wide range of programming language concepts, supporting rigorous analysis of their properties. Although it would require another book in itself to justify this assertion, these methods are also practical in that they are directly applicable to imple￾mentation and uniquely effective as a basis for mechanized reasoning. No other framework offers as much. Being a consolidation and distillation of decades of research, this book does not provide an exhaustive account of the history of the ideas that inform it. Suffice it to say that much of the de￾velopment is not original, but rather is largely a reformulation of what has gone before. The notes at the end of each chapter signpost the major developments, but are not intended as a complete guide to the literature. For further information and alternative perspectives, the reader is referred to such excellent sources as Constable (1986), Constable (1998), Girard (1989), Martin-Lof¨ (1984), Mitchell (1996), Pierce (2002, 2004), and Reynolds (1998). The book is divided into parts that are, in the main, independent of one another. Parts I and II, however, provide the foundation for the rest of the book, and must therefore be considered prior to all other parts. On first reading it may be best to skim Part I, and begin in earnest with Part II, returning to Part I for clarification of the logical framework in which the rest of the book is cast. Numerous people have read and commented on earlier editions of this book, and have sug￾gested corrections and improvements to it. I am particularly grateful to Umut Acar, Jesper Louis Andersen, Carlo Angiuli, Andrew Appel, Stephanie Balzer, Eric Bergstrom, Guy E. Blelloch, Il￾iano Cervesato, Lin Chase, Karl Crary, Rowan Davies, Derek Dreyer, Dan Licata, Zhong Shao