Andrés Goens
where else to find them
github:goens
what they talk about
all 4 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski3 editions2023–2026
- POPL2 editions2024–2026
on a stage with
all 15 in the filters
who talks about the same things
- Vijay Nagarajan4 talks
- Thomas Kœhler4 talks
- Michel Steuwer17 talks
- Guido Martínez10 talks
- Tobias Grosser14 talks
- Deepak Garg18 talks
| title | conference | date |
|---|---|---|
| A Formally Verified Foundation for Compositional Heterogeneous Coherence | PLDI 2026 | 2026-06-15 |
Claims that the de-facto Principle of Synchronous Propagation is sufficient to guarantee the Compound Memory Consistency Model for a wide class of CPU/GPU… | ||
| 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… | ||
| Guided Equality Saturation | POPL 2024 | 2024-01-14 |
Guided equality saturation splits a hard e-graph search into sequences of smaller equality-saturation runs guided by human-provided intermediate sketches… | ||
| Compound Memory Models | PLDI 2023 | 2023-06-17 |
Defines a compositional operational specification that composes distinct device models into a x86TSO/PTX compound model and proves C-to-architecture compiler… | ||
| nothing matches | ||