Jonathan Ragan-Kelley
where else to find them
no profile links on file
what they talk about
all 6 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski3 editions2024–2026
- OOPSLA3 editions2021–2025
all 5 in the filters
on a stage with
all 28 in the filters
who talks about the same things
- Adam Chlipala23 talks
- Gilbert Louis Bernstein9 talks
- Saman Amarasinghe13 talks
- Amanda Liu4 talks
- Mathieu Huot11 talks
- Manya Bansal4 talks
| title | conference | date |
|---|---|---|
| Modular GPU Programming with Typed Perspectives | PLDI 2026 | 2026-06-15 |
Prism is a low-level GPU language that tracks thread32 perspective and other granularities in types, exposes constructs like split and group and partition… | ||
| A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs | PLDI 2026 | 2026-06-15 |
Mechanized framework extends ATL and uses the Rock proof assistant to produce a verified compression/decompression adjoint that rewrites dense tensor kernels… | ||
| Bonsai: Compiling Queries to Pruned Tree Traversals | PLDI 2026 | 2026-06-15 |
Bonsai compiles high-level queries plus an annotated algebraic tree spec into C++ single-pass traversals that automatically generate always/maybe/never pruning… | ||
| A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning(…) | OOPSLA 2025 | 2025-10-16 |
Memo is a domain-specific probabilistic programming language for recursive theory-of-mind models that compiles to JAX and runs on GPUs. It embeds in Python… | ||
| Gauguin, Descartes, Bayes: A Diurnal Golem's Brain | Onward! 2025 | 2025-10-12 |
Builds a small probabilistic program in Church that samples and conditions over program-space to infer its own source; uses a grammar-based generator, eval… | ||
| Lightweight and Locality-Aware Composition of Black-Box Subroutines | PLDI 2025 | 2025-06-16 |
A system called Fern enriches black-box subroutine interfaces with producer-consumer annotations that describe how small data blocks are produced and consumed… | ||
| A Domain-Specific PPL for Reasoning about Reasoning (or: a memo on memo) | LAFI 2025 | 2025-01-19 |
Introduces memo, a Python-embedded domain-specific PPL that replaces sample/infer with choose/observe semantics and compiles recursive theory-of-mind models… | ||
| Distributions for Compositionally Differentiating Parametric Discontinuities | OOPSLA 2024 | 2024-10-20 |
Introduces Potto prototype as the first differentiable first-order language that soundly differentiates parametric discontinuities, gives a denotational… | ||
| A Verified Compiler for a Functional Tensor Language | PLDI 2024 | 2024-06-24 |
A mechanically verified implementation of a lowering algorithm for ATL proves that a functional tensor program lowers to imperative loop nests that write… | ||
| The Future of Fast Code: Giving Hardware What It Wants | PLDI 2024 | 2024-06-24 |
Hardware offers huge gains but only with heavy specialization: simple Python matrix multiply hits ~10 MFLOPS, JavaScript ~500 MFLOPS, optimized C reaches ~1–40… | ||
| Verified Tensor-Program Optimization Via High-Level Scheduling Rewrites | POPL 2022 | 2022-01-16 |
A Coq-verified framework implements a pure functional tensor IR called ATL and a suite of semantics-preserving, source-to-source rewrites plus reshape… | ||
| Efficient Automatic Scheduling of Imaging & Vision Pipelines for the GPU | OOPSLA 2021 | 2021-10-17 |
An autoscheduler generates GPU code from Halide algorithm code by combining a two-phase search that freezes low-cost stages, hierarchical sampling that groups… | ||
| nothing matches | ||