Leonardo de Moura
where else to find them
no profile links on file
what they talk about
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2022–2025
- ICFP2 editions2020–2022
on a stage with
- Daniel Selsamonce
- Michael Emmionce
- Sebastian Ullrichonce
all 4 in the filters
who talks about the same things
- Kenji Maillard11 talks
- Paulo Emílio de Vilhena5 talks
- Steve Zdancewic19 talks
- Nada Amin26 talks
- Cătălin Hriţcu16 talks
- Guido Martínez10 talks
| title | conference | date |
|---|---|---|
| Lean: Machine-Checked Mathematics and Verified Programming, Past and Future | PLDI 2025 | 2025-06-16 |
Lean claims a small trusted core and full extensibility, with 2 million lines in Mathlib and 100,000 theorems verified; automation like grinds and a verified… | ||
| "do" Unchained: Embracing Local Imperativity in a Purely Functional Langua... | ICFP 2022 | 2022-09-11 |
Adds local mutation, early return and iteration to do notation and provides formal translation rules that compile them to pure code while preserving semantics… | ||
| Recursion Synthesis with Unrealizability Witnesses | PLDI 2022 | 2022-06-13 |
Procedure synthesizes recursive functions by combining syntax-guided synthesis with a new functional unrealizability checker that emits counterexample… | ||
| Sealing Pointer-Based Optimizations Behind Pure Functions | ICFP 2020 | 2020-08-23 |
Shows how dependent types seal pointer tricks behind pure interfaces to turn exponential tree traversals into linear-time algorithms, implemented for Lean v4… | ||
| nothing matches | ||