0;95;0c Introduction to Program Synthesis

6.S981 Introduction to Program Synthesis Fall 2023

© Armando Solar-Lezama. 2023. All rights reserved.

Introduction to program synthesis

Lecture0:Slide1; Lecture0:Slide2; Lecture0:Slide3; Lecture0:Slide4; Lecture0:Slide5; Lecture0:Slide6


Welcome to 6.S981!
When/Where: TR1-2:30 in room 26-328

Join on Piazza.
Friday 11/17: Assignment 3 is now posted. You can find it here.

Tuesday 10/17 I came down sick so I won't be able to lecture today, but Kavi will have office hours at the usual class time and place.

Tuesday 9/26 and 9/28: I forgot to mention in lecture last week that I am traveling again this week so the 9/26 and 9/28 lectures will be on zoom again.

Thursday 9/14: As mentioned in class on Tuesday, the lecture today will be on zoom. Also, the first assignment has now be released. You can find it here.

Course description

This course aims to give an introduction to program synthesis, a new field at the intersection of programming languages, formal methods and AI. The course will explore a number of fundamental questions around the problem of how to automatically discover programs that do what the user expects. In particular, the class will explore the following questions:


The course will be graded based on three hands-on assignments as well as a final project where you will get to apply the concepts learned in the course to the problem of your choice. We are in discussions with the department to allow the course to count as a TQE in substitution of 6.820; should have final confirmation in the next couple of weeks. All psets are due at 5pm on the posted day. The late penalty will be 10 points per day up to a maximum of 4 days.


An important part of the grade will be a term project where students will demonstrate their mastery of the topics covered in the course. The projects can apply concepts from the course to a new problem, or explore new techniqes. The project grade be based on the following benchmarks:

The webpages for earlier versions of this course can be found here and here.