Instructor Contact Info
Course Mailing List
Programming in SML
Announcements/UpdatesThe first class will be on Tuesday, Sept. 29, 2009 at 1:30pm in Ry 251.
The Midterm Exam will take place in class on Thursday, November 5.
The Final Exam will take place on Tuesday, December 8 from 1:30pm to 3:30pm in Ry 251.
Instructor Contact Info
Name Role Office Office hours Phone David MacQueen Professor Ryerson 250 By appointment 2-4980 email@example.com
Course DescriptionProgramming languages are the most fundamental tools involved in the creation of software, and thus play a key role in computing. This is a foundational course exploring the principles and concepts underlying the design of programming languages. We use a formal approach based on operational semantics to give clear and precise descriptions of language concepts, such as flow of control, data structures and types, modularity and abstraction, and concurrency. The major paradigms of imperative, functional, and object-oriented paradigms will be covered, though the functional paradigm will be the main focus because of its simplicity.
Students should have experience programming in one or more programming languages, and familiarity with basic concepts of naive set theory and logic would be helpful. Inductive definitions and inductive proofs will play a central role.
The course is being taught as a combinded graduate/undergraduate course this year. There will be additional reading and assignments for the graduate students.
Course TextbookThe main textbook for the course is Programming Languages: Theory and Practice (2005 Edition) by Robert Harper. This is available in two versions as pdf files: online.pdf suitable for online viewing, or offline.pdf suitable for printing. Note that this is a different (and older) version of the book from what was originally posted on this page.
Other references that are useful for background material or further study are:
- Types and Programming Languages, by Benjamin Pierce, MIT Press, 2002, ISBN 0-262-16209-1. A thorough and readable reference emphasizing type systems.
- Discrete Structures, Logic, and Computability by James Hein. Covers relevant topics in set theory, logic, and discrete math. Used as a textbook in CMSC 15300, Foundations of Software.
- Naive Set Theory by Paul Halmos, Springer, 2001, ISBN 3540900926. A republished edition of a classic introductory text on the basics of set theory.
This is not a course centered on programming projects, but programming examples and exercises that show how to implement the ideas expressed in operational semantics will be given using the language Standard ML. There are several good sources of documentation and tutorials for SML/NJ available online, and some of these are given in the course SML/NJ page.
- Grading will be based on the following:
- Homework exercises: 40%
- Midterm exam: 25%
- Final exam: 35%
- Assigments: Homework assignments will normally be given on Tuesdays and will be due at the beginning of class the following Tuesday. Late homework can be handed in the class following the due date with a 30% penalty.
- Collaboration: As in most courses, we encourage students to discuss course material among themselves. Discussions of assignment problems is also permitted to an extent, but submitted assignments should be your own work, and collaborative discussions should be acknowledged.
- Final Examination: The final examination will be a two hour in-class exam given at 1:30pm on Dec 6 (time/date to be confirmed).
Course Mailing ListA mailing list has been created for the course. The address is firstname.lastname@example.org. The web page for the mailing list is at a https://mailman.cs.uchicago.edu/mailman/listinfo/cmsc22100.
Here are links to PDF files of the homework assignments (to be supplied).
Homework 1 (due Tuesday, Oct 13);
Homework 1 solution;
Homework 2 (due Tuesday, Oct 20);
Homework 2 solution (revised) (with the original version, which covers Problem 3;
Homework 3 (due Thursday, Oct 29);
Homework 3 solution;
Homework 3, Problem 5 programming solution (arith-SOS-oper.sml);
Homework 4 (due Thursday, Nov 12);
Homework 4 solution;
Homework 5 (due Tuesday, Nov 24);
Homework 6 (due Tuesday, Dec 1);
Here are links to PDF files of the handouts.
Rule Induction for Arith+Let
with LaTeX source files: arith-ind.tex, Static and Dynamic semantics of Arith.
Description of dynamic and static semantics of the C-machine.
Description of the E-machine.
Description of Landin's SECD machine.
Mathias Blume Notes from 2008
Supplementary lecture notes.
An Overview of Standard ML.
Homework 1 solutions.
Homework 1 comments.
Here are links to sample code.
arith.sml: arithmetic with let, calculating free variables
arith-interp.sml: simple interpreter for arithmetic with let (single variable substitutions)
arith-SOS.sml: SOS-style evaluator for arithmetic using substitutions
arith-ENV.sml: environment-based evaluator for arithmetic
arith-EV.sml: EV-style evaluator for arithmetic using substitutions
arith.scm: environment-based evaluator for arithmetic (scheme version)
Type checker and evaluator for MiniML
Big-step evaluator for pure lambda calculus
Big-step evaluator for pure lambda calculus (alternate version)
Evaluator for lambda calculus using environments
Tarball of code for Reynolds "Definitional Interpreters" paper
C-machine evaluator for MinML
E-machine evaluator for MinML
SECD machine evaluator for MinML
SECD compiler for MinML
E-machine evaluator for MinML with products
Type checker and evaluator for MinML with recursive types
Interactive interpreter for extended MinML (tarball)
Papers and PresentationsThe Mechanical Evaluation of Expressions by Peter Landin (Computer Journal, 1964)
The Next 700 Programming Languages by Peter Landin (CACM, 1966)
Definitional Interpreters for Higher-Order Progamming Languages by John Reynolds (1972)
The Revised Report on the Syntactic Theories of Sequential Control and State by Matthias Felleisen and Robert Hieb
A Functional Correspondence Between Evaluators and Abstract Machines by Olivier Danvy et al.
From Interpreter to Compiler and Abstract Machine by Olivier Danvy et al.
A Structural Approach to Operational Semantics by Gordon Plotkin.
The Discoveries of Continuations by John Reynolds.
Structure and Abstraction in HOT Languages (Marktoberdorf Summer School Notes, 2000).
Additional Useful LinksFrank Pfenning at CMU has a web site for his version of a course 15-312 Foundations of Programming Languages based on Harpers draft book. This web site has some very useful supplementary lecture notes (found under the Schedule page), as well as assignments, software, and other resources. You may find it useful to browse through this site and download some of the material.