Home
WebLog
News
Articles
Book Reviews
Field Report
Editors

Center

Page

Web

Wiki

Log In or Register

Programming Language Theory Texts Online

Techno

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