eecs 762: programming languages foundations i
fall 2019

essentials | homework | final | schedule


Instructor J. Garrett Morris
Office Eaton 2028
Office hours WF 10—11 PM, and by appointment
Course website
Lectures MWF 9:00—9:50 AM, Learned Hall 1136
Textbook Aaron Stump, Programming Language Foundations


This course is an introduction to modern approaches to the semantics of programming languages. The course will introduce denotational, axiomatic, and operational approaches to defining the semantics of simple programming languages. It will also introduce the mathematical techniques necessary for using these approaches, including the study of domains and continuous functions and of proof systems and logics. Finally, we will discuss the λ-calculus, a simple model of computation that underlies modern functional programming languages, and its connections to logic and proof theory.

The syllabus is available here. The syllabus spells out the details of grading, expectations, and so forth.


Homework and solutions are no longer available

Number Due date Assignment Sample solutions
1 Monday, September 9, 9:00 AM [pdf] [tex] [pdf] [tex]
2 Monday, September 23, 9:00 AM [pdf] [tex] [pdf] [tex]
3 Monday, October 7, 9:00 AM [pdf] [tex] [pdf] [tex]
4 Monday, October 28, 9:00 AM [pdf] [tex] [pdf] [tex]
5 Monday, November 11, 9:00 AM [pdf] [tex] [pdf] [tex]
6 Monday, November 25, 9:00 AM [pdf] [tex] [pdf] [tex]
7 Wednesday, December 18, 11:59 PM [pdf] [tex]

midterm review

The midterm review is available [pdf] [tex], and the soultions are similarly available [pdf] [tex]. To typeset the solutions, you will also need infer.sty, my preferred package for typesetting inference rules and proofs. The review questions are harder than the ones you should expect on the exam.

final examination

In lieu of a written final examination, the final will take the form of a lecture on a programming languages paper from the list below.


You will select one paper from the list below, and prepare a 30–35 minute lecture on that paper. Your lecture should be sufficient to explain the high-level results of the paper, and give some idea of the techniques used to achieve those results; you do not need to present all the results of the paper in depth (and indeed, do not have the time to do so).

While these papers all draw on the material of the course, each of them will go beyond the course material. You should expect to do some background research on the material in the paper. You should include this background material in your presentation.

You may use whatever presentation materials best suit your material and lecture. You should focus on the material, rather than the presentation itself: a well-made slide deck that you do not understand, or does not address the paper, will do you very little good. That said, I expect a minimum of preparation; scrolling awkwardly around the PDF of the paper is not acceptable.

Several of the papers have common background material, or build on each other. If these papers are selected, I will order the presentations accordingly. You should talk to each other to attempt to minimize overlap in presentations.

paper selection

Papers will be selected in class on October 28. I will ask you for your selections in a randomized order. Duplicate selections will not be allowed.

To help prepare for paper selection, the fourth homework assignment asks you to prepare short summaries of two of the papers. You should take this opportunity to make sure your selected paper is something you find comprehensible and at least mildly interesting.

presentation dates

Presentations will take place during the final 4 days of class (December 4, 6, 9 and 11). Unless constrained by paper material, presentation order will be random. Presentation order will be announced on October 30.

preliminary discussion

I will schedule a preliminary discussion with each of you, at least one week before your presentation. This should ensure that discussions are well-focused, include sufficient background, and go into enough depth. This can only be effective if you come to these discussions prepared, however. You should have, at the very least, a detailed outline of your presentation, if not having an initial drafts of your presentation materials. To encourage prepartion, the preliminary discussion is incorporated into your final grade.

Preliminary discussions will also be scheduled on October 30.


Your evaluation includes four components: your preparation for the preliminary discussion, your presentation itself, your answers to questions during your presentation, and the questions you ask during your classmates' presentations.

The final exam is worth 20% of the course grade. That 20% will be divided among those components as follows.

A more detailed rubric for presentation grading will be released.

Preliminary discussion 5%
Presentation 9%
Questions (asked) 3%
Questions (answered) 3%



date topics reading notes
8/26 Introductions
Course objectives
Mathematical preliminaries
"Mathematical background" appendix Homework 1 out
8/28 FO(Z) term syntax and formal semantics 1.1, 1.2, 1.6
8/30 FO(Z) formula syntax and formal semantics
Validity and satisfiability
1.3, 1.5, 1.7
9/2 No lecture.
9/4 Simple induction 1.10
9/6 Simple induction (continued).
Structural induction.
9/9 while syntax and semantics.
The problem with loops
2.1, 2.2, 2.3 Homework 2 out
9/11 Partially-ordered sets
2.4.1, 2.4.3
9/13 ω-chains
2.4.2, 2.4.4
9/16 Continuous functions 2.5
9/18 Kleene's fixed point theorem 2.6
9/20 Semantics of loops 2.7
9/23 No lecture Homework 3 out
9/25 Denotational equivalence 3.1
9/27 Partial correctness assertions
Rules and derivations
3.2, 3.3
9/30 Hoare logic 3.4, 3.5
10/2 Soundness of Hoare logic 3.6
10/4 Relative completeness of Hoare logic 3.6.1
10/7 Midterm review
10/9 Midterm exam
10/11 Big-step operational semantics
No movie—sorry! We'll get to Matt eventually.
10/14 No lecture
10/16 Final presentation discussion
Relating operational and denotational semantics
Homework 4 out
10/18 Relating operational and denotational semantics (part 2)
10/21 λ-calculus
10/23 λ-encodings
Non-termination in λ-calculus
Capture avoiding substitution
5.2.5, 6.5, 5.2.1
10/25 Homework discussion
10/28 Small-step operational semantics
Contexts and reduction orders
5.2–5.4 Homework 5 out
10/30 Relating big-step and small-step operational semantics 5.6
11/1 Relating big-step and small-step operational semantics (ctd)
11/4 PCF
Syntax of types
11/6 Term models of PCF types
Type assignment rules
7.2, 7.3
11/8 Soundness
11/11 Equational theory of PCF
Frame models
Homework 6 out
11/13 Adding recursion to PCF
11/15 Recursion in frame models
11/18 Soundness (ctd) Adequacy
11/20 Adequacy
11/22 Presentation discussions
11/25 Movie night: Matt Might on error Homework 7 out
No class—Thanksgiving break
12/2 Presentation #0
12/4 Presentation: Andrei on Wadler's Propositions as Types
12/6 Presentation: Andrew on Felleisen's Expressiveness of Programming Languages
12/9 Presentation: Kailani on Ramsay & Pfeffer's Stochastic Lambda Calculus
12/11 Presentation: Dalton on Sabelfeld & Myers's Language-Based Information Flow Security