Schedule

Week 1

Tuesday, September 3

First day of class.

Thursday, September 5

• Introductory discussion.
• Presentation by Teaching Fellow Raffi Sanna.

Week 2

Tuesday, September 10

• TF Raffi Sanna continues his presentation.
• Prof. Nada Amin presents a quick demo of ChatGPT integrating tools like verifiers and solvers through GPT actions.

Thursday, September 12

We set the schedule for the course.

Week 3

Tuesday, September 17

Tutorial on implementing Simply-Typed Lambda Calculus (STLC) with iso-recursive types from formal semantics.

We will consider languages (paradigms) like Dafny (verified functional programming), miniKanren (relational programming), Coq (proof assistant), Idris (dependent types).

We will consider techniques for reasoning about binders, for defining operational semantics (small step vs big step), for representing functions/closures (first order vs higher order).

Preparation homework: read up on STLC and iso-recursive types. TAPL is a good source for both.

Relevant code links:

• In Dafny, STLC with iso-recursive types by Prof. Nada Amin.
• In miniKanren, the typing rules for the core STLC.
• In miniKanren, the big-step relational evaluator for the core STLC.

Thursday, September 19

Survey on techniques for reasoning about binders and scope, theoretically and practically.

Challenges include quotienting modulo alpha-equivalence, implementing capture-avoiding substitution, handling shadowing.

Techniques include nominal logic, higher-order abstract syntax (HOAS), de Bruijn index, locally nameless, combinatory logic (which avoids variables entirely).

Preparation homework: dive into a specific technique, and be ready to share insights and code snippets.

Week 4

Tuesday, September 24

Alvan leads a session on probabilistic programming.

Paper of the day (POPL’23): ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs (paper, code).

Thursday, September 26

Matthew R. leads a session on neuro-symbolic programming.

Paper of the day (PLDI’23): Scallop: A Language for Neurosymbolic Programming (paper, code).

Week 5

Tuesday, October 1

Ulrik and Matt lead a session on theorem proving and machine learning.

Tentative paper of the day (NeurIPS’18): Reinforcement Learning of Theorem Proving (PDF). See also more recent work by first author, Cezary Kaliszy, highlighted in his CPP’24 keynote (video).

TODO for leaders: please explore the theme, and confirm the paper of the day. I recall the current paper is a bit low on technical details, but maybe that’s OK if you supplement with your own research. Also send a pull request with more resources below.

Resources on automated theorem proving: leanTAP.

Thursday, October 3

Raffi will lead a session on binders.

Preparation homework: Look at the definition of capture-avoiding substitution as laid out in the assignment. Try and find a few examples on which CAS is undefined. What happens if we try to evaluate them naively (just replacing all the variables by name)? Can you use the α-equivalence rule to convert your examples into terms on which CAS is defined?

The slides for this session are available here.

Week 6

Tuesday, October 8

Dennis leads a session on Hoare logic and how to semi-automatically verify it via verification conditions.

Paper of the day (FM’23): HHLPy: Practical Verification of Hybrid Systems using Hoare Logic (PDF, code)

Pointers on Hoare Logic:

• CS152 Lecture Notes
• CACM’69: An axiomatic basis for computer programming by C. A. R. Hoare
• Fifty years of Hoare’s logic

Thursday, October 10

Alex B. leads a session on Rust verification.

System of the day: Verus (code, playground, guide, VerusBench (hand-written examples)). Recent papers:

• SOSP’24: Verus: A Practical Foundation for Systems Verification (accepted draft in shepherding, code for case studies)
• OOPSLA’23: Verus: Verifying Rust Programs using Linear Ghost Types (PDF).

Optional extra paper of the day (ICFP’22): Aeneas: Rust Verification by Functional Translation (PDF, code).

Week 7

Tuesday, October 15

Introductory session on multi-stage programming led by Prof. Nada Amin and guest Cameron Wong, who will also discuss related ongoing research.

Paper of the day (JFP’19): A SQL to C compiler in 500 lines of code (PDF, code).

Extra pointers on multi-stage programming

All bolded projects might be touched upon in class demos.

Projects using Scala/LMS:

• LMS: Lightweight Modular Staging (CACM’12, tutorials)
• LMS-Verify (POPL’17 PDF, code)
• Collapsing Towers of Interpreters (POPL’18 PDF, code)
• Collapsing Towers for Side-Channel Security (Draft TBD, code)
• GenSym (ICSE’23 PDF, code)

Multi-stage programming in other languages/systems:

• MetaOCaml
• BuildIt in C++ (CGO’21 PDF, code, online demo) – the lead Ajay Brahmakshatriya gives a talk at the Harvard PL seminar on Friday, October 18 (2:00-3:15 in SEC 6.412)
• staged-miniKanren (Draft TBD)

Some PL theory of multi-stage programming:

• Two-level type theory (Google Scholar search)
• λ-calculus λ°: A Temporal Logic Approach to Binding-Time Analysis (Rowan Davies, 2017)

Thursday, October 17 (Assignment 1 Due)

Alex C. leads a session on multi-stage programming.

Paper of the day (ICFP’22): András Kovács, Staged Compilation With Two-Level Type Theory (PDF, code, appendix)

Week 8

Tuesday, October 22

Albert and Howard lead a session on algebraic effects.

Paper of the day (POPL’17): Do be do be do (paper, code).

Thursday, October 24

Daniel and Dashiell lead a session on HoTT.

Readings of the day:

• Read Sections 2.1-2.4 + 2.10 of the HoTT book (PDF),
• Peek at Cubical Agda.

Additional resources:

• Introduction to Homotopy Type Theory by Rijke (PDF: an alternative to the HoTT book more focused on a bottom-up deriviation of concepts in mathematics within HoTT.
• Videos by Emily Riehl, overviewing category theory behind HoTT: 1, 2, 3.

Week 9

Tuesday, October 29 (Project Proposals Due)

Guest lecture by Michael Ballantyne on reconciling optimizing compilation and extensibility.

• Paper of the day (ICFP’24 Functional Pearl): Compiled, Extensible, Multi-language DSLs (paper, code).
• Optional paper on the broader picture of Racket’s language-oriented programming (CACM’18): A Programmable Programming Language.

Thursday, October 31

Saketh and Suki lead a session on LLMs and mathematical discovery.

Paper of the day (NeurIPS’24): Learning Formal Mathematics From Intrinsic Motivation by Gabriel Poesia, David Broman, Nick Haber and Noah D. Goodman (paper, code)

Week 10

Tuesday, November 5

Guest lecture by William Byrd on midoriKanren.

Paper of the day: as a warm-up, read this programming pearl on Quine Generation via Relational Interpreters (PDF).

Thursday, November 7

Guest lecture by Kartik Chandra (MIT) around memo, a new probabilistic programming language for expressing computational cognitive models.

Paper of the day: shared draft on Ed. Feedback encouraged.

Week 11

Tuesday, November 12

Alice leads a session.

Paper of the day (PLDI’24): Bit Blasting Probabilistic Programs (PDF, code).

Thursday, November 14

Wolfie leads a session on the TACO tensor algebra compiler.

Paper of the day (OOPSLA’17): The Tensor Algebra Compiler (PDF). See all project papers.

Week 12

Student Presentations of their Ongoing Projects

Each student has 10 minutes to pitch their project and get feedback. The pitch should motivate, describe and situate the project and outline a plan for the rest of semester. What challenges do you anticipate? What milestones do you hope to achieve? How will you evaluate success? Feel free to structure your pitch to maximize feedback from the class.

Tuesday, November 19

1. Alex C.
2. Wolfie
3. Albert
4. Dennis
5. Alice
6. Suki
7. Howard

Thursday, November 21

1. Dashiell
2. Ulrik
3. Daniel
4. Matt
5. Saketh (postponed)
6. Matthew
7. Alvan

Week 13

Tuesday, November 26

Project workout.

Thursday, November 28

Thanksgiving.

Week 14

Tuesday, December 3

Last day of class.

Guest speaker McCoy Becker (MIT) will lead a session on probabilistic programming.

Paper of the Day (PLDI’24): Probabilistic Programming with Programmable Variational Inference