Practical foundations for programming languages

"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."--Provided by publisher "This book offers a fresh perspective on the fundamentals of programming languages through the use of type theory"-- "Syntactic Objects Programming languages are languages, a means of expressing computations in a form comprehensible to both people and machines. The syntax of a language specifies the means by which various sorts of phrases (expressions, commands, declarations, and so forth) may be combined to form programs. But what sort of thing are these phrases? What is a program made of? The informal concept of syntax may be seen to involve several distinct concepts. The surface, or concrete, syntax is concerned with how phrases are entered and displayed on a computer. The surface syntax is usually thought of as given by strings of characters from some alphabet (say, ASCII or Unicode). The structural, or abstract, syntax is concerned with the struc- 4 1.1 Abstract Syntax Trees ture of phrases, specifically how they are composed from other phrases. At this level a phrase is a tree, called an abstract syntax tree, whose nodes are operators that combine several phrases to form another phrase. The binding structure of syntax is concerned with the introduction and use of identifiers: how they are declared, and how declared identifiers are to be used. At this level phrases are abstract binding trees, which enrich abstract syntax trees with the concepts of binding and scope. We will not concern ourselves in this book with matters of concrete syntax, but will instead work at the level of abstract syntax. To prepare the ground for the rest of the book, we begin in this chapter by definin-ing abstract syntax trees and abstract binding trees and some functions and relations associated with them. The definitions are a bit technical, but are absolutely fundamental to what follows. It is probably best to skim this chapter on first reading, returning to it only as the need arises"-- 1. Judgment and rules 2. Statics and dynamics 3. Total functions 4. Finite data types 5. Types and propositions 6. Infinite data types 7. Variable types 8. Partiality and recursive types 9. Dynamic types 10. Subtyping 11. Dynamic dispatch 12. Control flow 13. Symbolic data 14. Mutable state 15. Parallelism 16. Concurrency and distribution 17. Modularity 18. Equational reasoning 19. Appendices. This book defines and analyzes a full range of programming language concepts in a single unifying framework that isolates core abstractions and avoids irrelevant details of specific languages. It stresses the central role of types and teaches the use of rigorous mathematical techniques for proving properties of languages and programs.