Armando Solar-Lezama Home

Research Agenda:

I lead the Computer Assisted Programming Group . The focus of our research is program synthesis, an exciting research area that lies at the intersection of Programming Systems and Artificial Intelligence. On the one hand, program synthesis is about the use of automated reasoning and learning to help bring more automation to the programming process. On the other hand, we believe code provides a uniquely versatile modeling mechanism, so program synthesis can play a powerful role in helping to build learning systems that are more predictable and robust.

Sketch Version 1.7.6 Released (Feb, 2020) :

Sketch has now moved to github and is split between two repositories: the sketch-backend and the sketch-frontend. You can download an easy-to-install (relatively speaking) source distribution from here: sketch-1.7.6.tar.gz

Working version of Sketch Manual
If you want to be notified about new releases or major bug-fixes, you can subscribe to the sketch users mailing list

Teaching:

Over the last few years, I have helped with the development of a few courses:

Program Synthesis: Everything you wanted to know about the state of the art in program synthesis, especially the techniques developed by the programming languages and formal methods communities. Here are some lecture notes I put together while on sabbatical in Mexico City in 2018.
6.820--Foundations of Program Analysis: This is an introduction to many of the core techniques that one can use to reason about programs, including different forms of semantics, type systems, program logics, abstract interpretation and model checking. And you also learn Haskell along the way! The course is offered every 2 years. The class was last offered in 2021.
6.s081-- Dynamic Computer Language Engineering: Michael Carbin has been mostly leading this class, but I helped with the initial version of it. In this class, students get to build a just-in-time compiler for a non-trivial dynamic language completely from scratch. See here for a recent version of this class.

In recent years, I have also been involved in teaching 6.031 (Software Construction), 6.009 (Fundamentals of Programming) and 6.01 (Introduction to EECS via Robotics).

PlaySkript:

In my free time, I created PlaySkript, an online platform that I use for creating presentations and visualizations. It's based on a JavaScript-like domain specific language for describing diagrams and animations, and supports both direct manipulation and automated refactoring in order to help create complex presentations more easily. Try it out!

Phd Thesis:

Program Synthesis by Sketching, U.C. Berkeley, December 2008, Advisor: Rastislav Bodik

Contact:

MIT Computer Science and Artificial Intelligence Laboratory
The Stata Center, Building 32-G742
32 Vassar Street
Cambridge, MA 02139
Assistant: Amanda Abrams ()

Accessibility

Research Agenda:

Sketch Version 1.7.6 Released (Feb, 2020) :

Teaching:

PlaySkript:

Phd Thesis:

Conference Papers

Journal and Journal/Conferences

Technical Reports

Contact: