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.)
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:
- 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.
- 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.
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.