Practical Foundations for Programming Languages

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.

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).

Table of Contents

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

Book Details

Subject
Computer Science
Publisher
Carnegie Mellon University
Published
2012
Pages
590
Edition
1
Language
English
PDF Size
3.0 MB
License
CC BY-NC-ND

Related Books

Introduction to Programming with Fortran
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...
Programming Languages and Systems
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 ...
Data Parallel C++
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...
Foundations of Software Science and Computation Structures
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...
Principles of Programming Languages
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...
Fundamental Approaches to Software Engineering
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 ...