Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

YouTube

Automated Proof Generation for Associative and Distributive Rewriting with E-Graphs

ACM SIGPLAN via YouTube

Overview

Explore a 22-minute video presentation from the EGRAPHS 2024 workshop that delves into automated proof generation for associative and distributive rewriting using e-graphs. Learn about a novel strategy for encoding a dependently-typed inductive language within e-graphs, originally designed for proof assistants. Discover how the presenters tackle automated reasoning about distributivity and associativity by encoding their domain-specific language into egglog. Gain insights into the challenges of proof extraction in egglog and the proposed strategies for building proof trees and implementing extraction in Metatheory.jl. Understand the future plans to interface with Coq for automating proof generation and checking, potentially reducing the overhead in using Coq libraries and enabling broader reasoning about distributive and associative structures.

Syllabus

[EGRAPHS24] Automated Proof Generation for Associative and Distributive Rewriting with E-Graphs

Taught by

ACM SIGPLAN

Reviews

Start your review of Automated Proof Generation for Associative and Distributive Rewriting with E-Graphs

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.