fall 2019

Instructor |
J. Garrett Morris |

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

You will need to log in with your KU username to access homework assignments and solutions.

Number |
Due date |
Assignment |
Sample solutions |

1 | Monday, September 9, 9:00 AM | [pdf] [tex] | |

2 | Monday, September 23, 9:00 AM | [pdf] [tex] |

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 | Labor day–no class. |
||

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 |