Robert Harper - Practical Foundations for Programming Languages

This text develops a comprehensive theory of programming languages based ontype systems and structural operational semantics. Language concepts are preciselydefined by their static and dynamic semantics, presenting the essential tools bothintuitively and rigorously while relying on only elementary mathematics. Thesetools are used to analyze and prove properties of languages and provide theframework for combining and comparing language features. The broad range ofconcepts includes fundamental data types such as sums and products, polymorphicand abstract types, dynamic typing, dynamic dispatch, subtyping and refinementtypes, symbols and dynamic classification, parallelism and cost semantics, andconcurrency and distribution. The methods are directly applicable to languageimplementation, to the development of logics for reasoning about programs, and tothe formal verification language properties such as type safety.

This thoroughly revised second edition includes exercises at the end of nearlyevery chapter and a new chapter on type refinements.

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