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

YouTube

Bridging Syntax and Semantics of Lean Expressions in E-Graphs

ACM SIGPLAN via YouTube

Overview

Explore a 28-minute video presentation from the EGRAPHS 2024 workshop that delves into bridging the gap between Lean's expression semantics and syntactically driven e-graphs in equality saturation. Discover how Marcus Rossel and Andrés Goens from Technische Universität Dresden and the University of Amsterdam tackle the challenge of implementing proof automation for equational reasoning in Lean. Learn about their approach to handling bound variables, implicit typing, and Lean's definitional equality, which encompasses α-equivalence, β-reduction, and η-reduction. Gain insights into the challenges they face and their ongoing development efforts, including their partially unsound techniques that remain sound due to Lean's proof checking. Access the active development of this project on GitHub and understand its potential impact on reducing the time and effort required for theorem proving in interactive theorem provers like Isabelle/HOL, Coq, and Lean.

Syllabus

[EGRAPHS24] Bridging Syntax and Semantics of Lean Expressions in E-Graphs

Taught by

ACM SIGPLAN

Reviews

Start your review of Bridging Syntax and Semantics of Lean Expressions in 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.