Schedule

Please regularly check Ed for deadlines and assignments; the Ed schedule is authoritative.

Week 1

Thursday, September 3

First day of class.

Week 2

Tuesday, September 8

Reading: Peter Naur (1985), Programming as Theory Building (PDF)

Thursday, September 10

Reading: look at the Compiling to Neurons papers of Joey Velez-Ginorio, who will join as a guest. In particular, see the POPL’26 and PLDI’26 papers with Nada Amin, Konrad Kording, and Steve Zdancewic.

Week 3

Tuesday, September 15

Reading: Sverrir Thorgeirsson, Theo B. Weidmann, Zhendong Su (CHI’26), Computer Science Achievement and Writing Skills Predict Vibe Coding Proficiency (PDF)

Secondary reading: Kathi Fisler, Shriram Krishnamurthi, Michael Littman (CACM’26 to appear), Teaching Novice Computing and Programming in the Agentic AI Era, (link)

Thursday, September 17

Reading: Alex Gu, Naman Jain, Wen-Ding Li, Manish Shetty, Yijia Shao, Ziyang Li, Diyi Yang, Kevin Ellis, Koushik Sen, Armando Solar-Lezama (ICML 2025), Challenges and Paths Towards AI for Software Engineering (PDF)

Alex Gu will join as a guest.

Week 4

Tuesday, September 22

Reading: Gan Shen, Shun Kashiwa, Lindsey Kuper (ICFP 2024). HasChor: Functional Choreographic Programming for All (Functional Pearl) (doi)

PhD student Cameron Wong will talk about his experience implementing choreographic libraries in Lean.

Thursday, September 24

Reading: Simon Henniger, Stephen Chong, Nada Amin (2026). Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler (link)

Week 5

Tuesday, September 29

Class on formal verification.

Refresher: CS1520: Axiomatic Semantics and Hoare Logic (Lecture 19) and Curry-Howard correspondence (Lecture 15).

Reading 1 (for auto-active verifiers like Dafny): C. A. R. Hoare (CACM 1969). An axiomatic basis for computer programming (doi).

Reading 2 (for proof assistants like Lean or Rocq): Philip Wadler (CACM 2015). Propositions as Types (doi)

Thursday, October 1

Tzu-Han Hsu presented advanced verification and model checking.

Week 6

Tuesday, October 6 (Assignment 1 Due)

Discussion of assignment.

Thursday, October 8

Discussion of assignment.

Week 7

tuesday, october 13

Student presentations (see schedule on Ed).

Thursday, October 15

Reading: Bowers et al. (POPL 2023). Top-Down Synthesis for Library Learning (doi). Also see E-Stitch: Top-Down Library Learning for E-Graphs (2026) (link).

Maddy Bowers will be presenting and discussing her work related to library learning.

Week 8

Tuesday, October 20

Reading: Celeste Barnaby, Danny Ding, Osbert Bastani, Isil Dillig (PLDI 2026). Choose, Don’t Label: Multiple-Choice Query Synthesis for Program Disambiguation (PDF).

Celeste will join us as a guest for the session.

Thursday, October 22

Student presentations (see schedule on Ed).

Week 9

Tuesday, October 27

Student presentations (see schedule on Ed).

Thursday, October 29

Student presentations (see schedule on Ed).

Week 10

Tuesday, November 3

Student presentations (see schedule on Ed).

Thursday, November 5

Student presentations (see schedule on Ed).

Week 11

Tuesday, November 10

Student presentations (see schedule on Ed).

Thursday, November 12

Student presentations (see schedule on Ed).

Week 12

Tuesday, November 17

TBD

Thursday, November 19

TBD

Week 13

Tuesday, November 24

Final project presentations (schedule to be set shortly).

Thursday, November 26

Final project presentations (schedule to be set shortly).

Week 14

Tuesday, December 1

Final project presentations (schedule to be set shortly).