| Instructor | J. Garrett Morris |
| garrettm@ku.edu | |
| Office | Eaton 2028 |
| Office hours | MWF 10—11 PM, and by appointment |
| Course website | https://ittc.ku.edu/~garrett/eecs762f18/ |
| 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.
| 11/12 | Homework 6 is released. This is the final homework of the semester. It will be worth 1.5x the other homework assignments in determining your homework grade. |
| 9/5 | The due date for homework 2 has been extended to September 10. |
| 8/24 | The due date for homework 1 has been extended to September 4. This does not mean the next homework will be delayed; it will still be assigned on August 27 |
| 8/20 | Welcome to EECS 762! Homework 1, including TeX sources, is posted. |
Homework and solutions are no longer available.
| Number | Due date | Assignment | Sample solutions |
| 1 | Tuesday, September 4, 9:00 AM | [pdf] [tex] | [pdf] [tex] |
| 2 | Monday, September 10, 9:00 AM | [pdf] [tex] | [pdf] [tex] |
| 3 | Monday, September 24, 9:00 AM | [pdf] [tex] | [pdf] [tex] |
| 4 | Monday, October 29, 9:00 AM | [pdf] [tex] | [pdf] [tex] |
| 5 | Monday, November 12, 9:00 AM | [pdf] [tex] | [pdf] [tex] |
| 6 | Wednesday, December 5, 9:00 AM | [pdf] [tex] | [pdf] [tex] |
| date | topics | reading | notes |
| 8/20 |
Introductions Course objectives Mathematical preliminaries |
"Mathematical background" appendix | Homework 1 out |
| 8/22 | $FO(\mathbb Z)$ syntax and informal semantics | 1.1–1.5 | |
| 8/24 |
$FO(\mathbb Z)$ formal semantics Validity and satisfiability |
1.6–1.9 | |
| 8/27 |
$FO(\mathbb Z)$ formal semantics Induction (weak and strong) |
1.10 | Homework 2 out |
| 8/29 | Induction (strong and structural) | 1.10–1.11 | |
| 8/31 | Induction (structural) The while language | 1.11, 2.1–2.3 | |
| 9/5 | Partial orders, bounds, lattices | 2.4.1–2.4.3 | |
| 9/7 | Lattices and complete partial ordres, ω-chains, continuous functions | 2.4.3–2.5 | |
| 9/10 | Continuous functions; least fixed point theorem | 2.5–2.6 | Homework 3 out |
| 9/12 | Lifted domains; semantics of while | 2.7 | |
| 9/17 | Partial correctness assertions | 3.1-3.3 | |
| 9/19 | Rules and derivations | 3.4 | |
| 9/21,10/1 | Rules of Hoare logic | 3.4-3.5 | |
| 10/3 | Soundness of Hoare logic | 3.6 | |
| 10/5 | Relative completeness of Hoare logic | 3.6.1 | |
| 10/12,10/17 | Big-step and small-step operational semantics | 4.1-4.2 | |
| 10/19 | Equivalence of big-step and small-step semantics | 4.3 | Homework 4 out |
| 10/22 | Equivalence of big-step and small-step operational semantics | 4.3 | |
| 10/24 | λ-calculus syntax and semantics | 5.1–5.2 | |
| 10/26 |
Capture-avoiding substitution β-reduction |
5.1–5.2 | |
| 10/29 |
β-reduction Non-termination Reduction order and contexts |
5.2 | Homework 5 out |
| 10/31 |
Reduction order Contexts |
||
| 11/2 | Big-step semantics for λ-calculus | 5.6 | |
| 11/5 | λ-encodings: Booleans, pairs, sums | 6.1 | |
| 11/7 | Church-encodings: naturals, iteration | 6.1 | |
| 11/9 | Church-encodings: lists, iteration | ||
| 11/12 | Scott-encodings: naturals, fixed points | 6.2 | Homework 6 out. |
| 11/14 | Scott-encodings: lists, fixed points |