# eecs 762: programming languages foundations ifall 2018

## essentials

 Instructor J. Garrett Morris Email 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

## syllabus

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.

## announcements

 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

 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