Guido Martínez
where else to find them
no profile links on file
what they talk about
all 5 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2025–2026
- ICFP2 editions2020–2025
all 6 in the filters
on a stage with
all 38 in the filters
who talks about the same things
- Danel Ahman7 talks
- Nikhil Swamy14 talks
- Tahina Ramananandro8 talks
- Cătălin Hriţcu16 talks
- Aseem Rastogi7 talks
- Exequiel Rivas6 talks
| title | conference | date |
|---|---|---|
| The Next Frontier for AI-Generated Kernels: Correctness | PAgE 2026 | 2026-06-15 |
KernelBench’s fixed test suites let buggy kernels pass tests and even reject correct implementations; mutation testing finds racey softmaxes and trivial… | ||
| SIMT-Step Execution: A Flexible Operational Semantics For GPU Subgroup Behavior | PLDI 2026 | 2026-06-15 |
Formal operational semantics defines subgroup behavior using dynamic basic blocks and a spectrum classifying instructions as independent, synchronous, or… | ||
| 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… | ||
| Project Everest: Perspectives from Developing Industrial-Grade High-Assurance(…) | PLDI 2026 | 2026-06-15 |
Project Everest produces a verified TLS stack and crypto suite rather than promises: it yields 1.3 million lines of F source that build in two hours, emits… | ||
| Towards formally secure compilation of verified F* programs against unverified ML(…) | PriSC 2026 | 2026-01-11 |
Framework written and verified in F compiles terminating higher-order IO F programs to a deeply embedded ML-like language with an end-to-end mechanized proof… | ||
| SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F* | ICFP 2025 | 2025-10-12 |
SecRef is a secure-compilation framework for F that enforces verified programs’ assumptions about dynamically shared ML-style mutable references by inserting… | ||
| Kuiper: verified and efficient GPU programming | ARRAY 2025 | 2025-06-17 |
Kuiper is a verified GPU language that uses dependent types and concurrent separation logic (built on F★/Pulse) to guarantee memory safety and race freedom for… | ||
| PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs | PLDI 2025 | 2025-06-16 |
PulseCore is a new, mechanized concurrent separation logic implemented inside F★ that claims to support impredicative invariants and higher‑order ghost state… | ||
| Securing Verified IO Programs Against Unverified Code in F* | POPL 2024 | 2024-01-14 |
A verified secure compilation pipeline for F programs that perform IO, called SCIO, compiles verified code to a smaller F target and enforces assumptions at… | ||
| SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed ... | ICFP 2020 | 2020-08-23 |
SteelCore provides a semantics for CSL inside F, deriving Hoare rules from effectful non‑deterministic interleaving; it encodes computations as action trees… | ||
| nothing matches | ||