CMSC 22610
Implementation of Computer Languages I
Winter 2011

Resources

Standard ML

• Implementations
  • Standard ML of New Jersey (SML/NJ) — used for course project
  • MLton
  • MLKit
  • PolyML
• SML Books
  • ML for the Working Programmer, Lawrence Paulson
  • Elements of ML Programming, Jeffrey Ullman
  • The Definition of Standard ML (Revised), Robin Milner, Mads Tofte, Robert Harper, and David MacQueen — not for the faint of heart!
  • Programming in Standard ML, Bob Harper
• SML Tutorials
  • Standard ML Tutorial — slides from class
  • Programming in Standard ML, Bob Harper
  • Notes on Programming SML/NJ, Riccardo Pucella
  • A Gentle Introduction to ML, Andrew Cumming
  • Programming in Standard ML '97: An On-line Tutorial, Stephen Gilmore
• Libraries
  • Standard ML Basis Library — use $/basis.cm in CM files
  • SML/NJ Library — use $/smlnj-lib.cm in CM files
• Tools
  • ml-ulex and ml-antlr: (pdf) — use $/ml-lpt-lib.cm in CM files
  • ml-lex: (pdf)  (html)
  • ml-yacc: (pdf)  (html) — use $/ml-yacc-lib.cm in CM files
  • Compilation Manager (CM): (pdf)
• Coding standards
  • Style Guide — these are useful (and common) conventions among SML programmers, but the are not required for submitted code

Subversion

• Subversion home page
• Official documentation

Parsing

• LR Parsing, a tutorial on LR parsing by Al Aho and Steve Johnson from the June 1974 Computing Surveys.

Type Checking

• Basic Polymorphic Typechecking by Luca Cardelli, a tutorial on HM type checking.
• A Theory of Type Polymorphism in Programming by Robin Milner, the original published account of Hindley-Milner type checking.
• Principal type-schemes for functional programs by Luis Damas and Robin Milner, proves that Algorithm W produces the most general type scheme.
• Proofs about a Folklore Let-Polymorphic Type Inference Algorithm by Oukseh Lee and Kwangkeun Yi, describes and alternate "top-down" version of Algorithm W that is closer to how type checkers are actually implemented.
• Efficient ML Type Inference Using Ranked Type Variables by George Kuan and David MacQueen, proves the correctness of the technique of using lambda-depth ranking to control type closure.

Programming Language Description, Semantics

In the Fall 2010 edition of the Programming Languages course (CMSC 22100) we developed ways of rigorously describing the meaning of a programming language, which tells us how individual programs in the language should behave. The lecture notes, homework, and other material for this course are available at the course web site:

http://www.classes.cs.uchicago.edu/archive/2010/fall/22100-1/

During the course, a series of increasingly complex functional languages were developed, leading up to PTFun, a polymorphic language with recursive types, sums, and products (essentially the equivalent of datatypes). Several formal techniques are used to specify the execution (dynamic semantics) of these languages. The type systems are formally described using inference rules, and theorems establish the type safety of the languages.

A full ML implementation of the final language, renamed "Fun", is contained in the following tarball, fun.tgz. This implementation includes a lexer, a parser, a type-checker, and an evaluator, plus an interactive read-eval-print loop.