This is a collection of programming language theory texts and resources, all
of which are

**freely available** over the Internet.

Many valuable reference texts on programming language theory, previously only
available in paper form, have in recent years become publicly accessible from
the net. I list here the ones I know of; below that you will also find a much
broader list of lecture notes and tutorials, other interesting reading, plus a
collection of related resources.

# Obligatory plea

If you know of any other texts or resources which might belong here, please
add them to this list by editing this page.
(Does your submission belong in this list? See the

#SubmissionGuidelines.)

I hope other authors will also make an effort, when possible, to get their
books online, especially if the book goes out of print.

Part of the reason PL theory and advanced programming languages seem
impenetrable to other communities is that learning materials are hard to
obtain, or demand a sizeable investment of resources (time, money, ...) even
if the potential reader is only exploring the subject.

# Reference texts

Harold Abelson and

Gerald Jay Sussman with Julie Sussman.

**Structure and Interpretation of Computer Programs.**
(

MIT)

Hassan Ait-Kaci.

**Warren's Abstract Machine: A Tutorial Reconstruction.**
(

link)

Andrea Asperti and

Giussepe Longo.

**Categories, Types and Structures. An introduction to Category Theory for the working computer scientist.**
(

link)

Henk Barendregt.

**Lambda Calculi with Types.**
(

compressed PS)

--.

**The Lambda Calculus.**
(

currently broken link)

Michael Barr and

Charles Wells.

**Toposes, Triples and Theories.**
(

link)

Stanley N. Burris and H.P. Sankappanavar.

**A Course in Universal Algebra.**
(

link)

Hubert Comon,

**et al.**
**Tree Automata Techniques and Applications.**
(

link)

Reinhard Diestel.

**Graph Theory.**
(

link)

Raphael Finkel.

**Advanced Programming Language Design.**
(

link)

Dick Grune and

Ceriel J.H. Jacobs.

**Parsing Techniques - A Practical Guide.**
(

link)

Robert Harper.

**Programming Languages: Theory and Practice. (Draft)**
(

link)

Matthew Hennessy.

**Semantics of Programming Languages.**
(

gzipped PS/2up,

Andrew Pitts' course material)

N.D. Jones, C.K. Gomard and

P. Sestoft.

**Partial Evaluation and Automatic Program Generation.**
(

link)

Carroll Morgan.

**Programming from Specifications.**
(

link)

Susumu Hayashi and

Hiroshi Nakano.

**PX: A Computational Logic.**
(

PDF,

link)

Hanne Riis Nielson and

Flemming Nielson.

**Semantics With Applications: A Formal Introduction.**
(

link)

Bengt Nordstrom and

Kent Petersson and

Jan M. Smith.

**Programming in Martin-Lof's Type Theory: An Introduction.**
(

link)

Simon Peyton Jones and David R. Lester.

**Implementing functional languages: a tutorial.**
(

link,

compressed PS,

sources)

Rinus Plasmeijer and

Marko van Eekelen.

**Functional Programming and Parallel Graph Rewriting.**
(

link)

Scott F. Smith.

**Programming Languages.**
(

link)

Paul Taylor.

**Practical Foundations of Mathematics.**
(

link)

Simon Thompson.

**Type Theory and Functional Programming.**
(

link)

# Notes and tutorials

Luca Cardelli and

Peter Wegner.

**On understanding types, data abstraction and polymorphism.**
(

PS/letter,

PDF/letter,

PS/A4,

PDF/A4)

Giuseppe Castagna.

**Subtyping and Object-oriented Programming**.
(

course page,

gzipped PS)

Robert Constable.

**Typed Logic.**
(

link,

HTML,

PS)

Jean H. Gallier.

**Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi.**
(

compressed DVI)

--.

**Constructive Logics. Part II: Linear Logic and Proof Nets.**
(

link,

compressed DVI,

compressed PS)

--.

**On the Correspondence between Proofs and lambda-Terms.**
(

compressed PS)

Mike Gordon.

**Introduction to Functional Programming.**
(

link)

--.

**Specification and Verification I.**
(

link - 2000 ed.)

--.

**Specification and Verification II.**
(

link - 1999 ed.)

John Harrison.

**Introduction to Functional Programming (1996/7).**
(

link)

Achim Jung and

Samson Abramsky.
Domain Theory.
(

gzipped PS)

Alexander Kurz.

**Coalgebras and Modal Logic.**
(

link)

Per Martin-Lof.

**On the Meanings of the Logical Constants and the Justifications of the Logical Laws.**
(

link)

Bengt Nordstrom,

Kent Petersson and

Jan M. Smith.

**Martin-Lof's Type Theory.**
(

gzipped PS)

Lawrence C. Paulson.

**Foundations of Functional Programming.**
(

link)

Frank Pfenning.

**Automated Theorem Proving.**
(

link)

--.

**Computation and Deduction.**
(

link)

Wesley Phoa.

**An introduction to fibrations, topos theory, the effective topos and modest sets.**
(

gzipped PS)

Andrew M. Pitts.

**Lecture Notes on Types.**
(

link)

--.

**Operational Semantics and Program Equivalence.**
(

PS)

--.

**Categorical Logic.**
(

gzipped PS)

Gordon Plotkin.

**Pisa Notes (on Domain Theory).**
(

link,

gzipped PS,

gzipped PS/A4)

Giuseppe Rosolini.

**Sheaves.**
(gzipped PS:

A4,

US)

Helmut Schwichtenberg.

**Proof Theory.**
(

compressed PS,

compressed DVI)

Morten Heine B. Sorenson and

Pawel Urzyczyn.

**Lectures on the Curry-Howard Isomorphism.**
(gzipped PS)

Thomas Streicher.

**Fibred Categories.**
(

gzipped PS)

# Other texts

Texts in this section are interesting, though not directly
related to programming language theory.

G.J. Chaitin.

**The Unknowable.**
(

link)

Philip J. Koopman, Jr.
**Stack Computers: the new wave.**
(

link)

# Resources

If you are interested in these topics, you can find additional resources (mostly in the forms of technical articles and theses) via:

# Submission guidelines

Most importantly, any submission must include a URL to the full text of the
manuscript: this is not an

*online list of texts*,
but rather

*a list of online texts*.
Also, the text should be freely accessible; so, texts which belong to
some sort of private digital library (like the ACM Digital Library or
Elsevier's collection) are not admissible.

This list focuses on book-length reference works which treat major topics
in programming language theory, mathematical semantics and foundations,
particularly texts which have gone out of print. It would be nice if we could
assemble a set of texts which are representative of a master's degree
curriculum in programming language theory or computational mathematics.

On the other hand, do not dismiss interesting-looking material only
because it is too short, or because it does not treat a central topic, or
because it is too specific. If you know of something valuable which does not
quite fit the guidelines above, consider putting it in the

#OtherTexts category.

Dissertations, theses and technical articles are not really suitable for this
list, unless they provide an accessible (or: the unique) introduction to, or
tutorial for, a relatively broad and/or important topic. Conversely, a survey
would need to treat its topic in considerable depth to be included here.

Lecture notes and tutorials are acceptable, provided they are readable as
self-contained manuscripts. Because there are so many manuscripts here of this
type, please try to submit material which minimizes overlap with existing
entries.

# Administration

This Wiki page is adapted from my (

FrankAtanassow's)

PLT Online page.

For now, both versions will coexist
and I will probably add any updates to this page to my own page as well, and vice versa.
If this Wiki version sees a lot of activity and takes off, and does not evolve too far
from my original purpose (outlined in the

#SubmissionGuidelines above),
then I may trash my page and redirect page views to this Wiki.

--

FrankAtanassow - 23 Sep 2002