Home
WebLog
News
Articles
Book Reviews
Field Report
Editors
Programming Language Theory Texts Online

Techno
%TOC%

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.

#ReferenceTexts
---+ Reference texts

[[http://www-swiss.ai.mit.edu/~hal/hal.html][Harold Abelson]] and [[http://www-swiss.ai.mit.edu/~gjs/gjs.html][Gerald Jay Sussman]] with Julie Sussman.
*Structure and Interpretation of Computer Programs.*
([[http://mitpress.mit.edu/sicp/full-text/book/book.html][MIT]])

[[http://www.isg.sfu.ca/~hak/][Hassan Ait-Kaci]].
*Warren's Abstract Machine: A Tutorial Reconstruction.*
([[http://www.isg.sfu.ca/~hak/documents/wam.html][link]])


[[http://www.cs.unibo.it/~asperti/][Andrea Asperti]] and [[http://www.di.ens.fr/users/longo][Giussepe Longo]].
*Categories, Types and Structures. An introduction to Category Theory for the working computer scientist.*
([[http://www.di.ens.fr/users/longo/download.html][link]])

[[http://www.cs.kun.nl/~henk/][Henk Barendregt]].
*Lambda Calculi with Types.*
([[ftp://ftp.cs.kun.nl/pub/CompMath.Found/HBKJ.ps.Z][compressed PS]])

--.
*The Lambda Calculus.*
([[http://www.elpress.com/readittoc.jsp?Book=0444875085][currently broken link]])

[[http://euclid.math.mcgill.ca/~barr/][Michael Barr]] and [[http://www.cwru.edu/artsci/math/wells/][Charles Wells]].
*Toposes, Triples and Theories.*
([[http://www.cwru.edu/artsci/math/wells/pub/ttt.html][link]])

[[http://www.thoralf.uwaterloo.ca/][Stanley N. Burris]] and H.P. Sankappanavar.
*A Course in Universal Algebra.*
([[http://www.thoralf.uwaterloo.ca/htdocs/ualg.html][link]])

[[http://www.lsv.ens-cachan.fr/~comon/?lang=en][Hubert Comon]], *et al.*
*Tree Automata Techniques and Applications.*
([[http://www.grappa.univ-lille3.fr/tata/][link]])

[[http://www.math.uni-hamburg.de/home/diestel/][Reinhard Diestel]].
*Graph Theory.*
([[http://www.math.uni-hamburg.de/home/diestel/books/graph.theory/][link]]) 

[[http://www.cs.engr.uky.edu/~raphael/][Raphael Finkel]].
*Advanced Programming Language Design.*
([[http://www.awprofessional.com/catalog/product.asp?product_id={92E30B39-5D91-45F9-9919-D202BE6341F9}&selectDescTypeId={A80972E0-1077-4518-954C-44E43E341DF7}][link]])

[[http://www.cs.vu.nl/~dick/][Dick Grune]] and [[http://www.cs.vu.nl/~ceriel/][Ceriel J.H. Jacobs]].
*Parsing Techniques - A Practical Guide.*
([[http://www.cs.vu.nl/~dick/PTAPG.html][link]])

[[http://www-2.cs.cmu.edu/~rwh/][Robert Harper]].
*Programming Languages: Theory and Practice. (Draft)*
([[http://www-2.cs.cmu.edu/~rwh/plbook/][link]])

[[http://www.cogs.susx.ac.uk/users/matthewh/][Matthew Hennessy]].
*Semantics of Programming Languages.*
([[http://www.cogs.susx.ac.uk/users/matthewh/semnotes.ps.gz][gzipped PS/2up]], [[http://www.cl.cam.ac.uk/Teaching/2000/Semantics/][Andrew Pitts' course material]])

[[http://www.diku.dk/~neil/][N.D. Jones]], C.K. Gomard and [[http://www.dina.dk/~sestoft/][P. Sestoft]].
*Partial Evaluation and Automatic Program Generation.*
([[http://www.dina.dk/~sestoft/pebook/pebook.html][link]])

[[http://web.comlab.ox.ac.uk/oucl/people/carroll.morgan.html][Carroll Morgan]].
*Programming from Specifications.*
([[http://web.comlab.ox.ac.uk/oucl/publications/books/PfS/][link]])

[[http://kurt.cla.kobe-u.ac.jp/~hayashi/index-english.html][Susumu Hayashi]] and [[http://www602.math.ryukoku.ac.jp/~nakano][Hiroshi Nakano]].
*PX: A Computational Logic.*
([[http://www602.math.ryukoku.ac.jp/~nakano/papers/freePXbook.pdf][PDF]], [[http://kurt.cla.kobe-u.ac.jp/~hayashi/PXbook.html][link]])

[[http://www.daimi.au.dk/~hrn/][Hanne Riis Nielson]] and [[http://www.daimi.au.dk/~fn/][Flemming Nielson]].
*Semantics With Applications: A Formal Introduction.*
([[http://www.daimi.au.dk/~bra8130/Wiley_book/wiley.html][link]])

[[http://www.cs.chalmers.se/~bengt/][Bengt Nordstrom]] and [[http://www.cs.chalmers.se/~kentp/][Kent Petersson]] and [[http://www.cs.chalmers.se/~smith/][Jan M. Smith]].
*Programming in Martin-Lof's Type Theory: An Introduction.*
([[http://www.cs.chalmers.se/Cs/Research/Logic/book/][link]])

[[http://research.microsoft.com/Users/simonpj/][Simon Peyton Jones]] and David R. Lester.
*Implementing functional languages: a tutorial.*
([[http://www.research.microsoft.com/Users/simonpj/Papers/papers.html][link]],
[[http://www.research.microsoft.com/Users/simonpj/Papers/student.ps.gz][compressed PS]],
[[http://www.research.microsoft.com/Users/simonpj/Papers/pjlester-1.11.tar.Z][sources]])

[[http://www.cs.kun.nl/~rinus/][Rinus Plasmeijer]] and [[http://www.cs.kun.nl/~marko/][Marko van Eekelen]].
*Functional Programming and Parallel Graph Rewriting.*
([[http://www.cs.kun.nl/~clean/Manuals/Addison__Wesley_book/addison__wesley_book.html][link]])

[[http://www.cs.jhu.edu/~scott/][Scott F. Smith]].
*Programming Languages.*
([[http://www.cs.jhu.edu/~scott/plbook/][link]])

[[http://www.dcs.qmw.ac.uk/~pt/][Paul Taylor]].
*Practical Foundations of Mathematics.*
([[http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/][link]])

[[http://www.cs.ukc.ac.uk/people/staff/sjt/][Simon Thompson]].
*Type Theory and Functional Programming.*
([[http://www.cs.ukc.ac.uk/people/staff/sjt/TTFP/][link]])

#NotesAndTutorials
---+ Notes and tutorials

[[http://www.luca.demon.co.uk/][Luca Cardelli]] and [[http://www.cs.brown.edu/people/pw/][Peter Wegner]].
*On understanding types, data abstraction and polymorphism.*
([[http://research.microsoft.com/Users/luca/Papers/OnUnderstanding.ps][PS/letter]],
[[http://research.microsoft.com/Users/luca/Papers/OnUnderstanding.pdf][PDF/letter]],
[[http://research.microsoft.com/Users/luca/Papers/OnUnderstanding.A4.ps][PS/A4]],
[[http://research.microsoft.com/Users/luca/Papers/OnUnderstanding.A4.pdf][PDF/A4]])

[[http://www.di.ens.fr/~castagna/][Giuseppe Castagna]].
*Subtyping and Object-oriented Programming*.
([[http://www.di.ens.fr/~castagna/TEACHING/dea_ens.html][course page]],
[[ftp://ftp.ens.fr/pub/dmi/users/castagna/TEACHING/dea-spp.ps.gz][gzipped PS]])

[[http://www.cs.cornell.edu/home/rc/][Robert Constable]].
*Typed Logic.*
([[http://www.cs.cornell.edu/cs671-fa99/][link]],
[[http://www.cs.cornell.edu/cs671-fa99/typed%20logic/index.html][HTML]],
[[http://www.cs.cornell.edu/cs671-fa99/postscript%20files/mark99.ps][PS]])

[[http://www.cis.upenn.edu/~jean/home.html][Jean H. Gallier]].
*Constructive Logics. Part I: A Tutorial on Proof Systems and Typed lambda-Calculi.*
([[ftp://ftp.cis.upenn.edu/pub/papers/gallier/conslog1.dvi.Z][compressed DVI]])

--.
*Constructive Logics. Part II: Linear Logic and Proof Nets.*
([[http://www.cis.upenn.edu/~jean/gallier-old-pubs.html][link]],
[[http://www.cis.upenn.edu/~jean/gallier-old-pubs.html][compressed DVI]],
[[ftp://ftp.cis.upenn.edu/pub/papers/gallier/conslog2.ps.Z][compressed PS]])

--.
*On the Correspondence between Proofs and lambda-Terms.*
([[ftp://ftp.cis.upenn.edu/pub/papers/gallier/cahiers.ps.Z][compressed PS]])

[[http://www.cl.cam.ac.uk/users/mjcg/][Mike Gordon]].
*Introduction to Functional Programming.*
([[http://www.cl.cam.ac.uk/Teaching/FuncProg/FuncProg.html][link]])

--.
*Specification and Verification I.*
([[http://www.cl.cam.ac.uk/Teaching/2000/SpecVer1/][link - 2000 ed.]])

--.
*Specification and Verification II.*
([[http://www.cl.cam.ac.uk/Teaching/1999/SpecVer2/][link - 1999 ed.]])

[[http://www.cl.cam.ac.uk/users/jrh][John Harrison]].
*Introduction to Functional Programming (1996/7).*
([[http://www.cl.cam.ac.uk/Teaching/Lectures/funprog-jrh-1996/index.html][link]])

[[http://www.cs.bham.ac.uk/~axj][Achim Jung]] and [[http://www.dcs.ed.ac.uk/home/samson][Samson Abramsky]].
Domain Theory.
([[http://www.cs.bham.ac.uk/~axj/pub/papers/handy.ps.gz][gzipped PS]])

[[http://www.cwi.nl/~kurz][Alexander Kurz]].
*Coalgebras and Modal Logic.*
([[http://www.cwi.nl/~kurz/cml-esslli01.html][link]])

Per Martin-Lof.
*On the Meanings of the Logical Constants and the Justifications of the Logical Laws.*
([[http://www.cs.cornell.edu/cs671-fa99/martin.html][link]])

[[http://www.cs.chalmers.se/~bengt/][Bengt Nordstrom]],
[[http://www.cs.chalmers.se/~kentp/][Kent Petersson]] and
[[http://www.cs.chalmers.se/~smith/][Jan M. Smith]].
*Martin-Lof's Type Theory.*
([[ftp://ftp.cs.chalmers.se/pub/cs-reports/papers/smith/hlcs.ps.gz][gzipped PS]])

[[http://www.cl.cam.ac.uk/users/lcp/][Lawrence C. Paulson]].
*Foundations of Functional Programming.*
([[http://www.cl.cam.ac.uk/Teaching/2000/FoundsCS/][link]])

[[http://www.cs.cmu.edu/~fp/][Frank Pfenning]].
*Automated Theorem Proving.*
([[http://www.cs.cmu.edu/~fp/courses/atp/handouts.html][link]])

--.
*Computation and Deduction.*
([[http://www.cs.cmu.edu/~fp/courses/comp-ded/handouts.html][link]])

Wesley Phoa.
*An introduction to fibrations, topos theory, the effective topos and modest sets.*
([[http://www.lfcs.informatics.ed.ac.uk/reports/92/ECS-LFCS-92-208/ECS-LFCS-92-208.ps.gz][gzipped PS]])

[[http://www.cl.cam.ac.uk/~amp12/][Andrew M. Pitts]].
*Lecture Notes on Types.*
([[http://www.cl.cam.ac.uk/Teaching/2000/Types/][link]])

--.
*Operational Semantics and Program Equivalence.*
([[http://www-sop.inria.fr/oasis/Caminha00/opespe.ps][PS]])

--.
*Categorical Logic.*
([[ftp://ftp.cl.cam.ac.uk/papers/amp12/catl.ps.gz][gzipped PS]])

[[http://www.dcs.ed.ac.uk/home/gdp/][Gordon Plotkin]].
*Pisa Notes (on Domain Theory).*
([[http://www.dcs.ed.ac.uk/home/gdp/publications/][link]],
[[http://www.dcs.ed.ac.uk/home/gdp/publications/Domains.ps.gz][gzipped PS]],
[[http://www.dcs.ed.ac.uk/home/gdp/publications/Domains_a4.ps.gz][gzipped PS/A4]])

[[http://www.disi.unige.it/person/RosoliniG][Giuseppe Rosolini]].
*Sheaves.*
(gzipped PS:
[[http://jazz.pst.informatik.uni-muenchen.de/spring-school99/topos.ps.gz][A4]],
[[http://www.pst.informatik.uni-muenchen.de/spring-school99/topos_l.ps.gz][US]])

[[http://www.mathematik.uni-muenchen.de/~schwicht/][Helmut Schwichtenberg]].
*Proof Theory.*
([[http://www.mathematik.uni-muenchen.de/~schwicht/lectures/proofth/ss99/pt99.ps.Z][compressed PS]],
[[http://www.mathematik.uni-muenchen.de/~schwicht/lectures/proofth/ss99/pt99.dvi.Z][compressed DVI]])

[[http://www.diku.dk/users/rambo/][Morten Heine B. Sorenson]] and [[http://zls.mimuw.edu.pl/~urzy/home.html][Pawel Urzyczyn]].
*Lectures on the Curry-Howard Isomorphism.*
(gzipped PS)

[[http://www.mathematik.tu-darmstadt.de/~streicher/][Thomas Streicher]].
*Fibred Categories.*
([[http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/fib.ps.gz][gzipped PS]])

#OtherTexts
---+ Other texts

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

[[http://www.cs.umaine.edu/~chaitin][G.J. Chaitin]].
*The Unknowable.*
([[http://www.cs.umaine.edu/~chaitin/unknowable/index.html][link]])

[[http://www-2.cs.cmu.edu/~koopman][Philip J. Koopman, Jr.]]
*Stack Computers: the new wave.*
([[http://www.mathematik.tu-darmstadt.de/~streicher/FIBR/fib.ps.gz][link]])

#MoreResources
---+ Resources

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

   * [[http://citeseer.nj.nec.com/cs][NEC's CS ResearchIndex]]
   * Mark Leone's [[http://www.cs.cmu.edu/~mleone/language-research.html][Programming Language Research]] page
   * Mark Leone's [[http://www.cs.cmu.edu/afs/cs.cmu.edu/user/mleone/web/language-people.html][Researchers in Programming Languages and Compilers]] page
   * [[http://www.afm.sbu.ac.uk/fm/][WWW Virtual Library: Formal Methods]]
   * [[http://xxx.lanl.gov/archive/cs/intro.html][Computing Research Repository (CoRR)]]
   * [[http://www.dcs.qmw.ac.uk/SEL-HPC/Articles/][SEL-HPC]] is inactive, but still occasionally useful.
   * Indiana's [[http://www.cs.indiana.edu:800/cstr/search][Unified Computer Science TR Index (UCSTRI)]]
   * Cornell's [[http://cs-tr.cs.cornell.edu/][Networked Computer Science Technical Reference Library (NCSTRL)]]
   * [[http://liinwww.ira.uka.de/bibliography/index.html][The Collection of Computer Science Bibliographies]]
   * CMU's [[http://www.cs.cmu.edu/afs/cs.cmu.edu/user/jblythe/Mosaic/cs-reports.html][On-line CS Techreports]]
   * [[http://cora.whizbang.com][Cora Research Paper Search]]
   * [[http://www.coalgebra.net][Coalgebra network online library]]
   * Paderborn's [[http://www.uni-paderborn.de/fachbereich/AG/agmadh/WWW/english/scripts.html][Collection of Lecture Notes, Surveys and Papers]]
   * [[http://www.md.chalmers.se/~rjmh][John Hughes]]' [[http://www.md.chalmers.se/~rjmh/tutorials.html][tutorial papers in functional programming]]
   * [[http://www.google.com][Google]] is a good search engine for technical topics.
   * [[http://lambda.weblogs.com][Lambda the Ultimate]] is a weblog on programming languages. Amongst other things, it offers a list of [[http://lambda.weblogs.com/design-docs][language design]] documents and [[http://lambda.weblogs.com/papers][research papers]].
   * [[http://lsi.uniovi.es/~labra/APL.html][Advanced Programming Languages]] ([[http://lsi.uniovi.es/~labra][Jose Emilio Labra Gayo]])
   * a list of ProgrammingLanguages on this server
   * [[http://hypatia.dcs.qmw.ac.uk/][Hypatia]] (broken)
   * [[http://readscheme.org/][readscheme.org]]

#SubmissionGuidelines
---+ 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 (Main.FrankAtanassow's)
[[http://www.cs.uu.nl/~franka/ref][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.

-- Main.FrankAtanassow - 23 Sep 2002