TTh, 1:30 pm - 2:50 pm

Ryerson 251

IndexAnnouncements

Instructor Contact Info

Course Description

Course Textbooks

Programming Exercises

Course Policies

Course Mailing List

Lecture Notes

Homework Assignments

Handouts

Sample Code

Programming in SML

SML/NJ FAQ

## The first class will be on Tuesday, Sept. 28, 2009 at 1:30pm in Ry 251.

Announcements/UpdatesThe final exam will be held 1:30pm to 3:30pm on Tuesday, Dec. 7, 2010.

Instructor Contact Info

NameRoleOfficeOffice hoursPhoneDavid MacQueen Professor Ryerson 250 By appointment 2-4980 dbm@cs.uchicago.edu ## Programming 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, starting with the functional paradigm because of its simplicity. Programming exercises in Standard ML will help make the formal concepts more concrete.

Course DescriptionStudents 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. There will be additional reading and assignments for the graduate students that extend the core material.

## The main textbook for the course is

Course TextbookProgramming Languages: Theory and Practice(2005 Edition) by Robert Harper. This is available as a pdf file: Harper2005.pdf. Note that this is an older draft of Harper's programming language text, which is currently known as Practical Foundations for Programming Languages. I prefer the older draft because of its lighter, less formal treatment of inference rules.The secondary textbook is Transitions and Trees: An Introduction to Operational Semantics, by Hans Hüttel, which will be available from Seminary Coop Bookstore.

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 Computabilityby James Hein. This text covers relevant topics in set theory, logic, and discrete math and has been used as a textbook in CMSC 15300, Foundations of Software.Naive Set Theoryby Paul Halmos, Springer, 2001, ISBN 3540900926. A republished edition of a classic introductory text on basic set theory.

Programming ExercisesThis course is not centered on programming projects, but the operational semantics techniques used to formalize programming language concepts are easily translated to programs that implement the concepts. We will use the language Standard ML for such programming experiments. 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.

Course Policies

Gradingwill be based on the following:

- Homework exercises: 50%
- Midterm exam: 20%
- Final exam: 30%
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 any collaborative inputs should be acknowledged.Final Examination:The final examination will be a two hour in-class exam given during Finals week.## A mailing list has been created for the course. The address is cmsc22100@mailman.cs.uchicago.edu. The web page for the mailing list is at a https://mailman.cs.uchicago.edu/mailman/listinfo/cmsc22100.

Course Mailing List

Lecture NotesLecture 1 (Tuesday, 9/28)

Lecture 2, (pdf) (Thursday, 9/30)

Lecture 3 (Tuesday, 10/5)

Lecture 4 (Thursday, 10/7)

Lecture 5 (Thursday, 10/14)prog_2_2.sml; prog_2_4.sml; prog_2_4.smlLecture 6 (Thursday, 10/21)

prog_3_1.sml; prog_3_2.sml; prog_3_3.sml; prog_3_4.smlLecture 7 (Tuesday, 10/26)

Fun-CBV-tests.sml; Fun-CBN-tests.sml

Lecture 8 (Tuesday, 11/2)

prog_4_1.smlLecture 9 (Thursday, 11/11)

Lecture 10 (Tuesday, 11/16)

Lecture 11 (Tuesday, 11/30); state-monad.sml

Homework AssignmentsHere are links to PDF files of the homework assignments.

Homework 1 (due Thursday, Oct 7);

Homework 1 Solution. (deriv.sml (derivations in ML))

Homework 2 (due Tuesday, Oct 19);

Homework 2 Solution (hw_2_4.sml, CR-CK-correspondence.pdf)

Homework 3 (due Tuesday, Oct 26);

Homework 3 Solution (Hw 3.1 code: hw_3_1.sml, Hw 3.4 code: hw_3_4.sml)

Homework 4 (due Tuesday, Nov 9);

Homework 4 Solution (Hw 4.4 code: hw_4_4.sml)

Homework 5 (due Tuesday, Nov 16);

Homework 5 Solution (Hw 5.3 code: hw_5_3.sml, Hw 5.4 code: hw_5_4.sml)

Homework 6 (due Tuesday, Nov 23) (start with tfun.tgz);

Homework 6 Solution (hw6.tgz)

Homework 7 (due midnight, Thursday, Dec 2)

(start with hw6.tgz, or your own hw 6 solution;

use ptfunsyntax.sml for the reference abstract syntax, and ptfuntests.sml for test cases.)

Homework 7 Solution (hw7.tgz)

Midterm Solutions

HandoutsHere 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.

cs221-style.tex

Mathias Blume CMSC221 Notes from 2008Supplementary lecture notes.

An Overview of Standard ML.

Homework 1.

Homework 1 solutions.

Homework 1 comments.

Sample CodeHere are links to sample code.

fun-interp.tgz, a tarball containing a complete interactive interpreter for the Fun language.

calc.tgz, a tarball containing a complete interactive calculator for the minimal arithmetic expression language

bigcalc.tgz, a tarball containing an interactive calculator for a greatly expanded expression language including booleans, conditionals, variable declarations, function definitions

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 PresentationsWhy Undergraduates Should Learn the Principles of Programming Languagesby the ACM SIGPLAN Education Board.

The Mechanical Evaluation of Expressionsby Peter Landin (Computer Journal, 1964)

The Next 700 Programming Languagesby Peter Landin (CACM, 1966)

Definitional Interpreters for Higher-Order Progamming Languagesby John Reynolds (1972)

The Revised Report on the Syntactic Theories of Sequential Control and Stateby Matthias Felleisen and Robert Hieb

A Functional Correspondence Between Evaluators and Abstract Machinesby Olivier Danvy et al.

From Interpreter to Compiler and Abstract Machineby Olivier Danvy et al.

A Structural Approach to Operational Semanticsby Gordon Plotkin.

The Discoveries of Continuationsby John Reynolds.

Structure and Abstraction in HOT Languages(Marktoberdorf Summer School Notes, 2000).

## Frank 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.

Additional Useful Links

Dave MacQueen Last modified: Wed Dec 5 16:46:41 CST 2007