Marcus Rossel
where else to find them
github:marcusrossel
what they talk about
where they keep going back
no series more than once — all 3 in the filters
on a stage with
all 5 in the filters
who talks about the same things
- Rudi Schneider3 talks
- Thomas Kœhler4 talks
- Michel Steuwer17 talks
- Andrés Goens6 talks
- Max Willsey12 talks
- Jahrim Gabriele Cesario2 talks
| title | conference | date |
|---|---|---|
| Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…) | POPL 2026 | 2026-01-11 |
Presents a Lean tactic that translates theorems into conditional rewrite rules, runs equality saturation with egg on an e-graphs representation, and… | ||
| Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs | PLDI 2025 | 2025-06-16 |
E-graphs gain native support for bound variables by making e-classes functions over parameterized e-classes (slots) so alpha-equivalent terms share a single… | ||
| Bridging Syntax and Semantics of Lean Expressions in E-Graphs | EGRAPHS 2024 | 2024-06-24 |
Prototype proof automation encodes Lean expressions into egg and uses equality saturation (egg backend) to synthesize explanations that Lean then checks… | ||
| nothing matches | ||