Coding Information

Basic OCaml

For basic OCaml information including installation, IDE's, etc, see the PL I OCaml page.

The OCaml Manual

The manual is here. Let us give a high-level overview of sections of the manual we will be using in the course.

  • Part I is the tutorial introduction; we covered chapters 1 and most of 2 in PL I, we will also cover functors of chapter 2 in this course. Chapters 3-6 we will (still) be skipping.
  • Part II is the language reference where you can look up details if needed. We will be covering a few topics in the langugage extensions chapter: locally abstract types (8.5), First-class modules (8.6), and GADT's (8.11).
  • Part III documents the tools which you should not need to look at.
  • Part IV describes the libraries; we will be using more of the standard library modules this time around, look at the manual for reference on them.

Other OCaml Resources

  • The on-line book Real World OCaml has recently been updated to a new edition and contains very nice tutorial descriptions of some of the newer features. It uses some non-standard library extensions from Jane Street which is a bit of a disadvantage for us however as in class we will just stick to the built-in ones.
  • A more extensive set of libraries is found in the Batteries Included extension to OCaml. You need to download and install this extension to use the libraries.

The PL II FbDK for OCaml

We have added some extensions to the FbDK for coding projects of PL II. We will be putting up a dist link here when it is finished.

Z3

When we get to using the Z3 SMT solver we will put some information here, stay tuned.

Coq

When we get to using the Coq theorem prover we will put some information here.