Tue 14 Jun 2022 11:45 - 12:00 at Toucan - Thinking Alike Chair(s): Max Willsey
Tue 14 Jun 2022 23:45 - 00:00 at Toucan - Thinking Alike

We present ongoing work on the use of e-graphs for the transformation of certified programs produced by a deductive synthesiser for heap-manipulating programs. We develop a strategy for optimising proofs using the mechanisms of e-graphs, propose a novel e-class analysis over \emph{proof scripts}, and report on its capabilities and limitations.

Tue 14 Jun

Displayed time zone: Pacific Time (US & Canada) change

10:30 - 12:00
Thinking AlikeEGRAPHS at Toucan +12h
Chair(s): Max Willsey University of Washington
10:30
15m
Talk
Logging an Egg: Datalog on E-Graphs
EGRAPHS
Philip Zucker Draper Laboratory
Pre-print Media Attached
10:45
15m
Talk
Chasing an egg
EGRAPHS
Yihong Zhang University of Washington
Pre-print
11:00
15m
Talk
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
15m
Talk
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
15m
Talk
Equality Saturation as a Tactic for Proof Assistants
EGRAPHS
Andrés Goens the University of Edinburgh, Siddharth Bhat the University of Edinburgh
11:45
15m
Talk
Towards Optimising Certified Programs by Proof Rewriting
EGRAPHS
Kiran Gopinathan National University of Singapore, Ilya Sergey National University of Singapore
22:30 - 00:00
Thinking AlikeEGRAPHS at Toucan
22:30
15m
Talk
Logging an Egg: Datalog on E-Graphs
EGRAPHS
Philip Zucker Draper Laboratory
Pre-print Media Attached
22:45
15m
Talk
Chasing an egg
EGRAPHS
Yihong Zhang University of Washington
Pre-print
23:00
15m
Talk
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
15m
Talk
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
15m
Talk
Equality Saturation as a Tactic for Proof Assistants
EGRAPHS
Andrés Goens the University of Edinburgh, Siddharth Bhat the University of Edinburgh
23:45
15m
Talk
Towards Optimising Certified Programs by Proof Rewriting
EGRAPHS
Kiran Gopinathan National University of Singapore, Ilya Sergey National University of Singapore