Syllabus

Research Project Guide

Schedule

Day # Lecture Topic Partners Readings Deadline
W 7 Jan 1 Course Introduction
M 12 Jan 2 Syntax
W 14 Jan 3 Semantics
M 19 Jan No class - MLK Day Holiday
W 21 Jan 4 Types
M 26 Jan 5 Inductive Reasoning A1 Released
W 28 Jan 6 Sums and Recursion, Formally
M 2 Feb 7 Constructive Logic
W 4 Feb 8 Propositions as Types, Universal Types
Th 5 Feb A1 Due
F 6 Feb A2 Released
M 9 Feb 9 Existential Types, Higher Kinds
W 11 Feb 10 Dependent Types I
M 16 Feb 11 Dependent Types II A2 Due
W 18 Feb 12 Dependent Types III A3 Released
M 23 Feb 13 Metatheory
W 25 Feb 14 Imperative Programming **A3 Due
A4 Released
Project Guide Released**
Sa 28 Feb - Su 8 Mar No class - Spring Break
M 9 Mar 15 Imperative Program Analysis A4 Due
W 11 Mar 16 Exam
M 16 Mar 17 Memory Management and Ownership A5 Released
W 18 Mar 18 Borrowing in Rust, Fundamentals of Parallelism, Concurrency, and Distribution
Th 19 Mar Project Proposals Due
M 23 Mar 19 No class - read papers!
T 24 Mar A5 Due
W 25 Mar 20 No class - read papers!
M 30 Mar 21 1. Gradual Typing (Kei Rockwell)
  1. Garbage Collection Algorithms (Sam Hiken)
  2. AI-Assisted Verification with Interactive Synthesis (Rafe Symonds) | 1. Jania Vandevoorde
  3. Yi Wang
  4. Vanshika Singla | 1. Gradual Typing for Functional Languages
  5. Uniprocessor Garbage Collection Techniques (Sections 1 and 2)
  6. Dafny: An Automatic Program Verifier for Functional Correctness | Annotated Bibliography Drafts (for presentations scheduled on or after 6 Apr) Due | | W 1 Apr | 22 | 1. Compiler Verification (Amirali Ebrahimzadeh)
  7. Compiler Verification II (Scott Brinley)
  8. Abstract Interpretation for Program Analysis (Andre Osores) | 1. Connor Rose
  9. Ruijie Gao
  10. Lani Quach | 1. Correctness of a Compiler for Arithmetic Expressions
  11. Formal Verification of a Realistic Compiler
  12. Systematic Design of Program Analysis Frameworks | | | F 3 Apr | | | | | Annotated Bibliography Drafts (for first week presentations) Due | | M 6 Apr | 23 | 1. Separation Logic (Lani Quach)
  13. Dataflow Analysis on Control Flow Graphs (Yi Wang)
  14. Information Flow Control and Declassification (Logan Green) | 1. Andre Osores
  15. Yi Wang
  16. Amirali Ebrahimzadeh | | | | W 8 Apr | 24 | 1. Reflective Programming: Origins, Methods, and Applications (Jania Vandevoorde)
  17. Recursion in Dependent Type Theory (Ivan Wei)
  18. Algebraic Structures in PL Theory (Connor Rose) | 1. Kei Rockwell
  19. Tianyiming Jing
  20. Jerry Zhu | | | | M 13 Apr | 25 | 1. Neurosymbolic Program Synthesis (Vanshika Singla)
  21. SMT-Based Invariant Synthesis for Distributed Protocols (Jerry Y Zhu)
  22. Reactive Synthesis for Hardware (Ruijie Gao) | 1. Rafe Symonds
  23. Logan Green
  24. Scott Brinley | | | | W 15 Apr | 26 | 1. Low Code Programming Models (Tianyiming Jing)
  25. Course Wrap-Up and Special Topics by request (Cyrus Omar) | 1. Ivan Wei
  26. make requests on Piazza! | | | | F 17 Apr | | | | | Annotated Bibliography Final Versions Due | | F 30 Apr | | | | | Project Reports Due |

Office Hours

Office Hours Queue: https://eecsoh.eecs.umich.edu/queues/39ze3BAI7f0rpDiq1tFzW5GLPqK

Prof. Cyrus Omar (Instructor) — Tuesdays at 6-7pm in 4624 BBB or Virtual

Thomas Porter (GSI) — Thursdays at 11:30am-12:30pm in BBB Atrium (i.e. Tishman Hall) or Virtual