**by Robert Harper**

DescriptionTable of ContentsDetailsHashtagsReport an issue ### Book Description

Types are the central organizing principle of the theory of programming languages. Language features 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 implementation and uniquely effective as a basis for mechanized reasoning. No other framework offers as much. ### Table of Contents

### Book Details

### Related Books

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 implementation and uniquely effective as a basis for mechanized reasoning. No other framework offers as much.

This open book is licensed under a Creative Commons License (CC BY-NC-ND). You can download Practical Foundations for Programming Languages ebook for free in PDF format (3.0 MB).

Part I

Judgments and Rules

Chapter 1

Syntactic Objects

Chapter 2

Inductive Definitions

Chapter 3

Hypothetical and General Judgments

Part II

Statics and Dynamics

Chapter 4

Statics

Chapter 5

Dynamics

Chapter 6

Type Safety

Chapter 7

Evaluation Dynamics

Part III

Function Types

Chapter 8

Function Definitions and Values

Chapter 9

Godel's T

Chapter 10

Plotkin's PCF

Part IV

Finite Data Types

Chapter 11

Product Types

Chapter 12

Sum Types

Chapter 13

Pattern Matching

Chapter 14

Generic Programming

Part V

Infinite Data Types

Chapter 15

Inductive and Co-Inductive Types

Chapter 16

Recursive Types

Part VI

Dynamic Types

Chapter 17

The Untyped -Calculus

Chapter 18

Dynamic Typing

Chapter 19

Hybrid Typing

Part VII

Variable Types

Chapter 20

Girard's System F

Chapter 21

Abstract Types

Chapter 22

Constructors and Kinds

Part VIII

Subtyping

Chapter 23

Subtyping

Chapter 24

Singleton Kinds

Part IX

Classes and Methods

Chapter 25

Dynamic Dispatch

Chapter 26

Inheritance

Part X

Exceptions and Continuations

Chapter 27

Control Stacks

Chapter 28

Exceptions

Chapter 29

Continuations

Part XI

Types and Propositions

Chapter 30

Constructive Logic

Chapter 31

Classical Logic

Part XII

Symbols

Chapter 32

Symbols

Chapter 33

Fluid Binding

Chapter 34

Dynamic Classification

Part XIII

State

Chapter 35

Modernized Algol

Chapter 36

Assignable References

Part XIV

Laziness

Chapter 37

Lazy Evaluation

Chapter 38

Polarization

Part XV

Parallelism

Chapter 39

Nested Parallelism

Chapter 40

Futures and Speculations

Part XVI

Concurrency

Chapter 41

Process Calculus

Chapter 42

Concurrent Algol

Chapter 43

Distributed Algol

Part XVII

Modularity

Chapter 44

Components and Linking

Chapter 45

Type Abstractions and Type Classes

Chapter 46

Hierarchy and Parameterization

Part XVIII

Equational Reasoning

Chapter 47

Equational Reasoning for T

Chapter 48

Equational Reasoning for PCF

Chapter 49

Parametricity

Chapter 50

Process Equivalence

Part XIX

Appendices

Appendix A

Finite Sets and Finite Functions

Subject

Computer Science

Publisher

Carnegie Mellon University

Published

2012

Pages

590

Edition

1

Language

English

PDF Size

3.0 MB

License

This fourth Edition presents new examples on submodules, derived type i/o, object oriented programming, abstract interfaces and procedure pointers, C interop, sorting and searching, statistics and converting to more modern versions of Fortran.Key FeaturesHighlights the core language features of modern Fortran including data typing, array processing...

This book constitutes the proceedings of the 27th European Symposium on Programming, ESOP 2018, which took place in Thessaloniki, Greece in April 2018, held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018.
The 36 papers presented in this volume were carefully reviewed and selected from 114 submissions. The ...

Learn how to accelerate C++ programs using data parallelism. This open book enables C++ programmers to be at the forefront of this exciting and important new development that is helping to push computing to new levels. It is full of practical advice, detailed explanations, and code examples to illustrate key topics.
Data parallelism in C++ enables...

This book constitutes the proceedings of the 15th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2012, held as part of the joint European Conference on Theory and Practice of Software, ETAPS 2012, which took place in Tallinn, Estonia, in March/April 2012.
The 29 papers presented in this book toget...

In this open book, our goal is to study the fundamental concepts in programming languages, as opposed to learning a range of specific languages. Languages are easy to learn, it is the concepts behind them that are difficult. The basic features we study in turn include higher-order functions, data structures in the form of records and variants, muta...

This book constitutes the proceedings of the 21st International Conference on Fundamental Approaches to Software Engineering, FASE 2018, which took place in Thessaloniki, Greece in April 2018, held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018.The 19 papers presented in this volume were carefully reviewed ...