Tue 14 Jun 2022 23:00 - 23:15 at Toucan - Thinking Alike
E-graphs are great at representing huge spaces of programs — so long as each subterm is independent. If not, they blow up. In this talk, we’ll present our work on equality-constrained tree automata (ECTAs), which extend e-graphs with equality constraints between terms, and come with efficient algorithms for finding terms that satisfy the constraints. In work currently in submission, we used our ecta library to build a polymorphic type-driven program synthesizer which is $8x$ faster than the current state of the art, Hoogle+, while using an order of magnitude less code. This talk will focus on how to use ECTAs to encode problems in many domains that are less of a fit for e-graphs, including well-typed polymorphic programs, SAT, and terms with binders.
Tue 14 JunDisplayed time zone: Pacific Time (US & Canada) change
10:30 - 12:00 | |||
10:30 15mTalk | Logging an Egg: Datalog on E-Graphs EGRAPHS Philip Zucker Draper Laboratory Pre-print Media Attached | ||
10:45 15mTalk | Chasing an egg EGRAPHS Yihong Zhang University of Washington Pre-print | ||
11:00 15mTalk | ECTAs: E-Graphs Better (at Encoding) EGRAPHS James Koppel Massachusetts Institute of Technology, USA, Zheng Guo University of California, San Diego, Edsko de Vries Well-Typed LLP, Armando Solar-Lezama Massachusetts Institute of Technology, Nadia Polikarpova University of California at San Diego | ||
11:15 15mTalk | E-Graphs, VSAs, and Tree Automata: a Rosetta StoneVirtual EGRAPHS Yisu Remy Wang University of Washington, James Koppel Massachusetts Institute of Technology, USA, Altan Haan OctoML, Josh Pollock MIT CSAIL Link to publication Pre-print | ||
11:30 15mTalk | Equality Saturation as a Tactic for Proof Assistants EGRAPHS | ||
11:45 15mTalk | Towards Optimising Certified Programs by Proof Rewriting EGRAPHS | ||
22:30 - 00:00 | |||
22:30 15mTalk | Logging an Egg: Datalog on E-Graphs EGRAPHS Philip Zucker Draper Laboratory Pre-print Media Attached | ||
22:45 15mTalk | Chasing an egg EGRAPHS Yihong Zhang University of Washington Pre-print | ||
23:00 15mTalk | ECTAs: E-Graphs Better (at Encoding) EGRAPHS James Koppel Massachusetts Institute of Technology, USA, Zheng Guo University of California, San Diego, Edsko de Vries Well-Typed LLP, Armando Solar-Lezama Massachusetts Institute of Technology, Nadia Polikarpova University of California at San Diego | ||
23:15 15mTalk | E-Graphs, VSAs, and Tree Automata: a Rosetta StoneVirtual EGRAPHS Yisu Remy Wang University of Washington, James Koppel Massachusetts Institute of Technology, USA, Altan Haan OctoML, Josh Pollock MIT CSAIL Link to publication Pre-print | ||
23:30 15mTalk | Equality Saturation as a Tactic for Proof Assistants EGRAPHS | ||
23:45 15mTalk | Towards Optimising Certified Programs by Proof Rewriting EGRAPHS | ||