Practical Foundations for Programming Languages



Download free course Practical Foundations for Programming Languages, pdf file on 590 pages by Robert Harper.
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

  • Judgments and Rules
  • Syntactic Objects
  • Inductive Definitions
  • Hypothetical and General Judgments
  • Statics and Dynamics
  • Statics
  • Dynamics
  • Type Safety
  • Evaluation Dynamics
  • Function Types
  • Function Definitions and Values
  • Godel's T
  • Plotkin's PCF
  • Finite Data Types
  • Product Types
  • Sum Types
  • Pattern Matching
  • Generic Programming
  • Infinite Data Types
  • Inductive and Co-Inductive Types
  • Recursive Types
  • Dynamic Types
  • The Untyped -Calculus
  • Dynamic Typing
  • Hybrid Typing
  • Variable Types
  • Girard's System F
  • Abstract Types
  • Constructors and Kinds
  • Subtyping
  • Subtyping
  • Singleton Kinds
  • Classes and Methods
  • Dynamic Dispatch
  • Inheritance
  • Exceptions and Continuations
  • Control Stacks
  • Exceptions
  • Continuations
  • Types and Propositions
  • Constructive Logic
  • Classical Logic
  • Symbols
  • Symbols
  • Fluid Binding
  • Dynamic Classification
  • State
  • Modernized Algol
  • Assignable References
  • Laziness
  • Lazy Evaluation
  • Polarization
  • Parallelism
  • Nested Parallelism
  • Futures and Speculations
  • Concurrency
  • Process Calculus
  • Concurrent Algol
  • Distributed Algol
  • Modularity
  • Components and Linking
  • Type Abstractions and Type Classes
  • Hierarchy and Parameterization
  • Equational Reasoning
  • Equational Reasoning for T
  • Equational Reasoning for PCF
  • Parametricity
  • Process Equivalence
  • Appendices
  • Finite Sets and Finite Functions
Pages : 590
Size : 3.0 MB
File type : PDF
Downloads: 146
Created: 2022-02-03
License: CC BY-NC-ND
Author(s): Robert Harper
Practical Foundations for Programming Languages

Warning: Trying to access array offset on false in /home/tutovnfz/public_html/article.php on line 233

Others programming Tutorials

Programming Persistent Memory: A Comprehensive Guide for Developers

Is Parallel Programming Hard, And, If So, What Can You Do About It?

C Programming for Arduino

Programming for Computations - MATLAB/Octave

Programming for Computations - Python

Others related eBooks about Practical Foundations for Programming Languages

Problem Solving with Algorithms and Data Structures Using Python

THIS TEXTBOOK is about computer science. It is also about Python. However, there is much more. The study of algorithms and data structures is central to understanding what computer science is all about. Learning computer science is not unlike learning any other type of difficult subject matter. Th...

Neural Network Programming with Java

Vast quantities of data are produced every second. In this context, neural networks become..., download free Java tutorial in PDF (244 pages) created by Alan M.F. Souza ....

Mastering Python

Python is a dynamic programming language. It is known for its high readability and hence i..., download free Python tutorial in PDF (486 pages) created by Rick van Hattem ....

Programming Fundamentals: A Modular Structured Approach Using C++

This book is an introduction to computer programming using C++ as the language for writing programmes, and to solid, fundamental programming principles - including writing structured programmes, looping, data structures and iteration. ...

Introduction to Programming with Fortran

Download free course Introduction to Programming with Fortran, pdf file on 963 pages by Ian Chivers, Jane Sleightholme....

How to Make Mistakes in Python

Download free course How to Make Mistakes in Python, pdf file on 82 pages by Mike Pirnat....

Elementary Algorithms

This is a free book about elementary algorithms and data structures. This book doesn't only focus on an imperative (or procedural) approach, but also includes purely functional algorithms and data structures. It doesn't require readers to master any programming languages, because all the algorit...

Algorithms

Algorithms are the lifeblood of computer science. They are the machines that proofs build ..., download free Algorithms tutorial in PDF (472 pages) created by Jeff Erickson ....

: Advanced R

It is impossible to become expert in R in only one training course. Yet, this course aims at giving a wide understanding of many aspects of R. Some external resources will be referred to in this book for you to be able to deepen what you would have learned in this course....

Basic OOP in C++

Download C++ programming language courses about object-oriented programming (OOP), free training document in PDF by Eunsuk Kang and JeanYang....