Resources for
Types and Programming Languages

Course Materials

TAPL has been used in many kinds of courses. Here are links to some of them. (If you are teaching from TAPL and would be willing to have a link to your materials listed here, please let me know.)

Typechecker Implementations

A collection of working implementations (typecheckers and simple interpreters) is available for most of the calculi covered in the text. These implementations offer an environment for experimenting with the examples in the book and testing solutions to exercises. They have also been polished for readability and modifiability and have been used successfully by students in my courses as the basis of both small implementation exercises and larger course projects.

The implementations directory contains each checker in the form of a single bundle (tarred and gzipped) and as a collection of separate files.

The implementations are written in OCaml. The OCaml compiler is available at no cost through http://caml.inria.fr and installs easily on a variety of platforms.

Once you have downloaded the files for a particular checker and installed the OCaml compiler on your machine, you can build a running checker in two ways:

  1. If your system provides the make program (e.g., if you are running on any kind of Unix, or on a Windows system with the Cygwin package installed), simply type make on the command line to build an executable checker, or make test to build the checker and immediately use it to process the input file test.f.
  2. If you do not have make, you can build and execute the checker manually by issuing the following commands:
      ocamllex lexer.mll
      ocamlyacc -v parser.mly
      ocamlc -c support.mli
      ocamlc -c support.ml
      ocamlc -c syntax.mli
      ocamlc -c syntax.ml
      ocamlc -c core.mli
      ocamlc -c core.ml
      ocamlc -c parser.mli
      ocamlc -c parser.ml
      ocamlc -c lexer.ml
      ocamlc -c main.ml
      ocamlc -o f support.cmo syntax.cmo core.cmo parser.cmo lexer.cmo main.cmo
    
Whichever way you chose to build the checker, you can now use it to process an input file test.f by typing ./f test.f at the command line.

Types Forum

Readers of TAPL should also be aware of the Types Forum, an email list covering all aspects of type systems and their applications. The list is moderated to ensure reasonably low volume and a high signal-to-noise ratio in announcements and discussions. Archives and subscription instructions can be found at http://www.cis.upenn.edu/~bcpierce/types.