Ariel E. Kellison
where else to find them
linkedin:ariel-kellison-4968722b0
what they talk about
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2025
- CPP2 editions2022–2024
on a stage with
- Justin Hsu2×
- Andrew W. Appelonce
- David Bindelonce
all 4 in the filters
who talks about the same things
- Laura Zielinski2 talks
- Justin Hsu13 talks
- Santosh Nagarakatte7 talks
- Jay P. Lim2 talks
- Mridul Aanjaneya2 talks
- Marco Gaboardi18 talks
| title | conference | date |
|---|---|---|
| Future-Proofing Numerical Accuracy with Formal Specifications | RocqPL 2026 | 2026-01-17 |
Argues that making floating‑point assumptions explicit and parameterized preserves accuracy as hardware and formats diversify. Builds LA proof, a library of… | ||
| Bean: A Language for Backward Error Analysis | PLDI 2025 | 2025-06-16 |
Bean is a typed first-order language that encodes backward error via a graded coeffect system with strict linearity and a categorical semantics proving… | ||
| Numerical Fuzz: A Type System for Rounding Error Analysis | PLDI 2024 | 2024-06-24 |
A new functional language Λnum offers a linear type system plus a novel graded monad to track local floating‑point rounding error and a sensitivity analysis to… | ||
| VCFloat2: Floating-point error analysis in Coq | CPP 2024 | 2024-01-15 |
VCFloat2 is a Coq tool that automatically and soundly computes floating‑point round‑off error bounds with computational reflection, handling nonstandard… | ||
| A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem | CPP 2022 | 2022-01-17 |
States a direct constructive proof of the Steiner–Lehmus theorem that is fully machine-checked inside a constructive proof assistant, avoids the law of… | ||
| nothing matches | ||