CS 252r: Advanced Topics in Programming Languages

NOTE: Schedule is subject to change.

Lec.	Date	Topic	Notes/Readings
Logical Relations
1	Wed 30-Aug	Introduction; Strong Normalization	TAPL Chapter 12. Lecture notes.
Mon 4-Sep Labor Day (no class)
2	Wed 6-Sep	Contextual equivalence	Lecture notes.
3	Mon 11-Sep	Theorems for Free	Lecture notes.
4	Wed 13-Sep	Step-indexed logical relations	Lecture notes.
Bisimulation and Coinduction
5	Mon 18-Sep	Bisimulations	An Introduction to Bisimulation and Coinduction. Davide Sangiorgi, slides from the Microsoft Research Summer School on Concurrency, 2012. Practical coinduction. Kozen and Silva, Mathematical Structures in Computer Science, 2016.
6	Wed 20-Sep	Coinduction and induction
7	Mon 25-Sep	SecDev (no class/class outing!)
8	Wed 27-Sep	Coinductive proofs
Program Synthesis
9	Mon 2-Oct	Introduction to program logics	Lecture notes.
10	Wed 4-Oct	Counter-Example Guided Abstraction Refinement (CEGAR)	Presenter: Hao Slides available on request Lazy Abstraction. Henzinger, Jhala, Majumdar, and Sutra, POPL 2002.
Mon 9-Oct Columbus Day (no class)
11	Wed 11-Oct	Sketching via Counter-Example Guided Inductive Synthesis (CEGIS)	Presenter: Thomas Sketching Concurrent Data Structures. Solar-Lezama, Jones, and Bodi_k, PLDI 2008.
12	Mon 16-Oct	Example-based syntehsis	Presenter: Ezra Steve away Automating String Processing in Spreadsheets Using Input-Output Examples. Gulwani, POPL 2011.
13	Wed 18-Oct	Metasketches	Steve away Optimizing Synthesis with Metasketches. Bornholt, Torlak, Grossman, and Ceze, POPL 2016.
14	Mon 23-Oct	Machine-learning and example-based synthesis	Presenter: Dan A Machine Learning Framework for Programming by Example. Menon, Tamuz, Gulwani, Lampson, amd Kalai, ICML 2013. Syntax-Guided Synthesis. Alur, Bodik, Juniwal, Martin, Raghothaman, Seshia, Singh, Solar-Lezama, Torlak, and Udupa, FMCAD 2013 (additional reading; optional).
Secure Compilation
15	Wed 25-Oct	Secure Compilation Guarantees	Presenter: Gabbi On Modular and Fully-Abstract Compilation. Patrignani, Devriese, and Piessens.
16	Mon 30-Oct	Secure Compilation Guarantees	Presenter: Jack Steve away Secure compilation and hyperproperty preservation. Patrignani and Garg, CSF 2017.
17	Wed 1-Nov	Secure Compilation Guarantees	Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation. Juglaret, Hritcu, Azevedo de Amorim, Eng, and Pierce, CSF 2016.
18	Mon 6-Nov	Verified Compilation	Presenter: Luca Formal certification of a compiler back-end. Leroy, POPL 2006.
Program Analysis
19	Wed 8-Nov	Weighted Pushdown Systems	Presenter: Eric Weighted Pushdown Systems and their Application to Interprocedural Dataflow Analysis. Reps, Schwoon, and Jha, SAS 2003.
20	Mon 13-Nov	Recurrence Analysis	Compositional Recurrence Analysis Revisited. Kincaid, Breck, Boroujeni, and Reps, PLDI 2017.
21	Wed 15-Nov	Library analysis	Presenter: Aaron FlowTwist: efficient context-sensitive inside-out taint analysis for large codebases. Lerch, Hermann, Bodden, and Mezini, FSE 2014.
22	Mon 20-Nov	Bi-abduction	Compositional Shape Analysis by means of Bi-Abduction. Calcagno, Distefano, O'Hearn, and Yang, POPL 2009.
Thanksgiving Recess
23	Mon 27-Nov	Project presentations
24	Wed 29-Nov	Project presentations
	Mon 11-Dec		Final projects due..