EECS 490: Programming Languages

Fall 2020

Due to the ongoing pandemic, EECS 490 will be held fully online this semester. This is a challenging time for everyone, students and course staff alike, and not everyone is affected the same way or to the same extent. We will work to adapt to everyone's individual needs as best as we can. We ask for everyone to act with kindness and understanding during this time. It will be particularly important to reach out and build friend groups proactively, and when you do, to include those who may not yet know others in the course.

Students will gain a modern understanding of programming language design and implementation. The emphasis will be on building up from mathematical first principles and on understanding programming languages simultaneously as formal structures and as human-computer interfaces.

The purpose of this course is to change the way you think about programming and programming language design in ways that will remain relevant across the many technology hype cycles that you will encounter over the course of your careers.

See the syllabus for all of the details.

Schedule

Day	#	Lecture Topic	Deadline	Readings
Tue 1 Sep	1	Course Overview + Programming with Mathematical Expressions		RWO Guided Tour (through Records and Variants)
Thu 3 Sep	2	Recursive Datatypes and Recursion Schemes		Optional: Cornell CS 3110 Notes Ch. 4, RWO Lists and Patterns (through Tail Recursion)
Tue 8 Sep	3	Equational and Inductive Reasoning	A1 and Survey 1 out	Princeton COS 326 Notes on Reasoning About Programs
Thu 10 Sep	4	Notation, Structure, and Semantics
Tue 15 Sep	5	Types and Variables	A1 and Survey 1 due, A2 out
Thu 17 Sep	6	Functions, Products
Tue 22 Sep	7	Sums, Exceptions	A2 due, A3 out
Thu 24 Sep	8	Recursive Expressions
Tue 29 Sep	9	Recursive Types	A3 due, A4 out
Thu 1 Oct	10	Parametric Polymorphism
Tue 6 Oct	11	Modules and Abstract Data Types	A4 due, A5 out	Optional: Princeton COS326 Lecture 12b: Modules
Thu 8 Oct	12	Gradual Typing, Dynamic Tagging, and Typed Holes		Optional: What is Gradual Typing by Jeremy Siek
Tue 13 Oct	13	Constructive Logic (Proofs are Programs)	A5 due	Optional: Propositions as Types by Philip Wadler
Thu 15 Oct	14	Midterm (during lecture)
Tue 20 Oct	15	References, Side Effects, and Loops	A6 out	Optional: TAPL Ch. 13
Thu 22 Oct	16
Tue 27 Oct	17	Encapsulated Commands (e.g. Haskell's IO types)	A6 due, A7 out	Optional: Introduction to IO (Haskell Wiki)
Thu 29 Oct	18	Imperative Program Verification		Optional: CMU 17-654: Hoare Logic: Proving Programs Correct Optional: Washington CSE 331: Reasoning About Code (Hoare Logic)
Tue 3 Nov	19	No class - Election Day!		Michigan Voter Information Center
Thu 5 Nov	20	Imperative Program Verification II
Tue 10 Nov	21	Ownership and Borrowing in Rust I	A7 due, A8 out	Rust Book Ch. 4.1-4.2: Understanding Ownership
Thu 12 Nov	22	Ownership and Borrowing in Rust II
Tue 17 Nov	23	Parallelism and Cost Semantics	A8 due	Optional: PFPL Ch. 37-38
Thu 19 Nov	24	Concurrency	A9 out	Optional: PFPL Ch. 39
Tue 24 Nov		No class - Thanksgiving Break
Thu 26 Nov
Tue 1 Dec	25	Distributed Programming		Optional: PFPL Ch. 40
Thu 3 Dec	26	Special Topics: Macro Systems	A9 due	Optional: Macros - Rust Book
Tue 8 Dec	27	Special Topics: Functional Web Development		Optional: Meta Tic-Tac-Toe (code) in Reason
Final Exam - TBD

Day

Lecture Topic

Deadline

Readings

Tue 1 Sep

Course Overview + Programming with Mathematical Expressions

RWO Guided Tour (through Records and Variants)

Thu 3 Sep

Recursive Datatypes and Recursion Schemes

Optional: Cornell CS 3110 Notes Ch. 4, RWO Lists and Patterns (through Tail Recursion)

Tue 8 Sep

Equational and Inductive Reasoning

A1 and Survey 1 out

Princeton COS 326 Notes on Reasoning About Programs

Thu 10 Sep

Notation, Structure, and Semantics

Tue 15 Sep

Types and Variables

A1 and Survey 1 due, A2 out

Thu 17 Sep

Functions, Products

Tue 22 Sep

Sums, Exceptions

A2 due, A3 out

Thu 24 Sep

Recursive Expressions

Tue 29 Sep

Recursive Types

A3 due, A4 out

Thu 1 Oct

Parametric Polymorphism

Tue 6 Oct

Modules and Abstract Data Types

A4 due, A5 out

Optional: Princeton COS326 Lecture 12b: Modules

Thu 8 Oct

Gradual Typing, Dynamic Tagging, and Typed Holes

Optional: What is Gradual Typing by Jeremy Siek

Tue 13 Oct

Constructive Logic (Proofs are Programs)

A5 due

Optional: Propositions as Types by Philip Wadler

Thu 15 Oct

Midterm (during lecture)

Tue 20 Oct

References, Side Effects, and Loops

A6 out

Optional: TAPL Ch. 13

Thu 22 Oct

Tue 27 Oct

Encapsulated Commands (e.g. Haskell's IO types)

A6 due, A7 out

Optional: Introduction to IO (Haskell Wiki)

Thu 29 Oct

Imperative Program Verification

Optional: CMU 17-654: Hoare Logic: Proving Programs Correct
Optional: Washington CSE 331: Reasoning About Code (Hoare Logic)

Tue 3 Nov

No class - Election Day!

Michigan Voter Information Center

Thu 5 Nov

Imperative Program Verification II

Tue 10 Nov

Ownership and Borrowing in Rust I

A7 due, A8 out

Rust Book Ch. 4.1-4.2: Understanding Ownership

Thu 12 Nov

Ownership and Borrowing in Rust II

Tue 17 Nov

Parallelism and Cost Semantics

A8 due

Optional: PFPL Ch. 37-38

Thu 19 Nov

Concurrency

A9 out

Optional: PFPL Ch. 39

Tue 24 Nov

No class - Thanksgiving Break

Thu 26 Nov

Tue 1 Dec

Distributed Programming

Optional: PFPL Ch. 40

Thu 3 Dec

Special Topics: Macro Systems

A9 due

Optional: Macros - Rust Book

Tue 8 Dec

Special Topics: Functional Web Development

Optional: Meta Tic-Tac-Toe (code) in Reason

Final Exam - TBD

Instructor

comar@umich.edu

12:00-1:30pm, TTh

GSI

hkpotter@umich.edu

TBD

yunsoo@umich.edu

TBD

zhiyipan@umich.edu

TBD

reddyvis@umich.edu

TBD

Grader

sayghosh@umich.edu

EECS 490: Programming Languages

Schedule

People