Michel Steuwer
where else to find them
mastodon:@michel@mastodon.acm.org
what they talk about
all 7 in the filters
where they keep going back
- POPL2 editions2024–2026
- PLDI Workshop Honoring Andreas Podelski2 editions2025–2026
- ICFP2 editions2020–2025
all 10 in the filters
on a stage with
all 46 in the filters
who talks about the same things
- Deepak Garg18 talks
- Guido Martínez10 talks
- Derek Dreyer35 talks
- Philipp Schuster13 talks
- Tiark Rompf24 talks
- Thomas Kœhler4 talks
| title | conference | date |
|---|---|---|
| Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic | PLDI 2026 | 2026-06-15 |
Kuiper is an F library that uses Pulse-based separation logic to verify GPU kernels, extending the logic with forall+ connective and located resources to model… | ||
| 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… | ||
| Multiple Resumptions and Local Mutable State, Directly | ICFP 2025 | 2025-10-12 |
A compilation strategy and runtime implement lexical effect handlers that support multiple resumptions plus stack-allocated mutable state by using a linked… | ||
| Machine Learning Guided Equality Saturation | EGRAPHS 2025 | 2025-06-16 |
Equality saturation guides get generated by a small autoregressive tree transformer that decodes trees node‑by‑node with two cross‑attention encoders 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… | ||
| Slotted E-Graphs | EGRAPHS 2024 | 2024-06-24 |
Implementation builds a new e-graph variant where e-classes are parameterized e-classes that accept slots for bound names, so renaming or removing binders… | ||
| Shoggoth - A Formal Foundation for Strategic Rewriting | POPL 2024 | 2024-01-14 |
Provides a formal denotational semantics for System S and a big-step operational semantics that explicitly models divergence, proves computational soundness… | ||
| 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… | ||
| Structural Subtyping as Parametric Polymorphism | OOPSLA 2023 | 2023-10-23 |
Compares structural subtyping for records and variants with row and presence polymorphism and gives compositional translations that preserve types and… | ||
| Investigating Magic Numbers: Improving the Inlining Heuristic in the Glasgow ... | Haskell Symposium 2022 | 2022-09-15 |
Explores changing GHC’s hard-coded inliner “magic numbers” by turning ten tuning constants into parameters, compiling GHC with different settings and running a… | ||
| Idris2-Table: Evaluating dependently-typed tables with... (Extended Abstract) | TyDe 2022 | 2022-09-11 |
Built an Idris 2 library that encodes table schemas as dependent types and implements the Brown Benchmark for Table Types examples and programs, covering… | ||
| Generating High Performance Code for Irregular Data Structures using Dependent Types | FHPNC 2021 | 2021-08-22 |
Extends a data-parallel language with index-sequence types (nuts), a scoping primitive (lift_nut / lift_nuts) and dependent pairs so offsets and packed CSR… | ||
| DelayRepay: Delayed Execution for Kernel Fusion in Python | DLS 2020 | 2020-11-17 |
DelayRepay is a drop-in NumPy replacement that defers NumPy operations to build a delayed execution graph, fuses those nodes into single CUDA kernels via CuPy… | ||
| Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High... | ICFP 2020 | 2020-08-23 |
Functional languages RISE and ELEVATE rewrite high-level data-parallel programs into optimized low-level code, expressing tiling, fusion and loop-permutation… | ||
| High-Level Synthesis of Functional Patterns with Lift | ARRAY 2019 | 2019-06-22 |
Extends Lift with Lift to VHDL backend and new streaming and tiling patterns, generates synthesizable VHDL that runs on a Xilinx XC7Z010 prototype board… | ||
| nothing matches | ||