| Instructor | J. Garrett Morris |
| garrettm@ku.edu | |
| Office | Eaton 2028 |
| Office hours | WF 10—11 PM, and by appointment |
| Course website | https://ittc.ku.edu/~garrett/eecs762f19/ |
| 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] |
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.
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.
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.
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.
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. |
1.11 | |
| 9/9 |
while syntax and semantics. The problem with loops |
2.1, 2.2, 2.3 | Homework 2 out |
| 9/11 |
Partially-ordered sets Bounds |
2.4.1, 2.4.3 | |
| 9/13 |
ω-chains ω-cpos Domains |
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. |
4.1 | |
| 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) λ-calculus |
5.1 | |
| 10/21 |
λ-calculus λ-encodings |
6.1 | |
| 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 |
7.1 | |
| 11/6 |
Term models of PCF– types Type assignment rules |
7.2, 7.3 | |
| 11/8 |
Soundness Normalization |
7.4,7.5 | |
| 11/11 |
Equational theory of PCF– Frame models |
Homework 6 out | |
| 11/13 | Adding recursion to PCF | ||
| 11/15 |
Recursion in frame models Soundness |
||
| 11/18 | Soundness (ctd) Adequacy | ||
| 11/20 | Adequacy | ||
| 11/22 | Presentation discussions | ||
| 11/25 | Movie night: Matt Might on error | Homework 7 out | |
|
11/27 11/29 |
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 |