Nikhil Swamy
where else to find them
what they talk about
all 8 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2025–2026
- CPP2 editions2023–2026
- ICFP2 editions2020–2023
all 6 in the filters
on a stage with
all 41 in the filters
who talks about the same things
- Guido Martínez10 talks
- Aseem Rastogi7 talks
- Danel Ahman7 talks
- Tahina Ramananandro8 talks
- Aymeric Fromherz9 talks
- Gabriel Ebner6 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… | ||
| 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… | ||
| Business Meeting | CPP 2026 | 2026-01-12 |
Conference sees 178 registrations, the highest yet; program runs from 75 submissions with 27 accepted (about 36%), up from 51 last year. Review process uses a… | ||
| 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… | ||
| Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming | Dafny 2025 | 2025-01-19 |
Curated a reproducible dataset of about 600K lines and 32K top-level F definitions (extended to 940K lines and 54K defs) plus a program‑fragment checker that… | ||
| Welcome | ICFP 2023 | 2023-09-04 |
ICFP 2023 opens in Seattle with an acknowledgement of the traditional Salish lands and a QR code linking to an article about local Indigenous issues. The… | ||
| FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores | CPP 2023 | 2023-01-16 |
FastVer2 is a verified, concurrent monitor for the Faster key-value store: implemented in C (≈8,000 lines produced from ≈50,000 lines of F proofs) using the… | ||
| ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER | CPP 2023 | 2023-01-16 |
Claims a first formalization of ASN.1 DER with a mechanized proof of non-malleability and a verified compiler in F that uses the EverParse framework to produce… | ||
| Q*: Implementing Quantum Separation Logic in F* | PLanQC 2022 | 2022-09-15 |
Prototype implements quantum separation logic inside F using the Steel library and Z3 for automation, ports Quantum Lib, and adds four quantum actions… | ||
| 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 | ||