Declarative Program Analysis and Optimization

CS294-260, Spring 2024

This course aims to give students experience with some of the many declarative techniques for program analysis and optimization. In particular, we will study term rewriting systems, datalog, and equality saturation.


The topics of future weeks are subject to change.

Wk Date Topic
1 Wed 1-17 Welcome
2 Mon 1-22 Term Rewriting
Wed 1-24 Playing by the Rules: Rewriting as a practical optimisation technique in GHC Tianrui, Shreyas
3 Mon 1-29 Verifying and Improving Halide’s Term Rewriting System with Program Synthesis Federico, Manish, Charles
Wed 1-31 Achieving High Performance the Functional Way: Expressing High-Performance Optimizations as Rewrite Strategies Sora, Eric
4 Mon 2-05 Datalog
Wed 2-07 Doop: Strictly Declarative Specification of Sophisticated Points-to Analyses Manish, Shaokai
5 Mon 2-12 From Datalog to Flix: A Declarative Language for Fixed Points on Lattices Tianrui, Altan
Wed 2-14 Slog: Higher-Order, Data-Parallel Structured Deduction Jiwon, Altan
6 Mon 2-19 Holiday
Wed 2-21 Functional Programming with Datalog Tyler, Jeremy
7 Mon 2-26 E-Graphs and Equality Saturation
Wed 2-28 Efficient E-matching for SMT Solvers Federico, Jacob, Jiwon
8 Mon 3-04 Equality Saturation: A New Approach to Optimization Sora, Shaokai
Wed 3-06 babble: Learning Better Abstractions with E-Graphs and Anti-Unification Eric, Jacob
9 Mon 3-11 Automatic Datapath Optimization using E-Graphs Jeremy, Charles, Shreyas
Wed 3-13 ECTAs: Searching Entangled Program Spaces Altan, Tyler
10 Mon 3-18 No Class
Wed 3-20 Better Together: Unifying Datalog and Equality Saturation Max
Thu 3-21 EGRAPHS Community Lightning Talks
11 Mon 3-25 Spring Break
Wed 3-27 Spring Break
12 Mon 4-01 Project Proposals
Wed 4-03 No Class
13 Project Meetings
14 Project Meetings
15 Mon 4-22 Project Presentations
Wed 4-24 Project Presentations