Joseph W. Cutler
where else to find them
no profile links on file
what they talk about
all 4 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2024–2026
all 6 in the filters
on a stage with
all 27 in the filters
who talks about the same things
- Amal Ahmed25 talks
- Craig Disselkoen4 talks
- Steve Zdancewic19 talks
- Daniel Sainati2 talks
- Jonathan Ragan-Kelley12 talks
- Lars Birkedal35 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… | ||
| Typing Strictness | POPL 2026 | 2026-01-11 |
Proposes a refinement of strictness called intentional strictness and encodes it as a type-and-effect system for call-by-name and call-by-push-value, with a… | ||
| Getting the Most Out of POPL | PLMW @ POPL 2025 | 2025-01-19 |
Conference plan: 82 talks translate to about 13 hours of presentations; aim to spend roughly 40% of each day not watching talks to network and rest. Prioritize… | ||
| Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization | OOPSLA 2024 | 2024-10-20 |
Cedar defines a concise DSL, a Rust evaluation engine, and a Lean formal model that proves key properties; policies compile into SMT in the sound and complete… | ||
| Stream Types | PLDI 2024 | 2024-06-24 |
Proposes a type-theoretic foundation that lets ordinary list programs run as online stream processors by rejecting programs that need unbounded buffering and… | ||
| Improving the Stability of Type Safety Proofs in Dafny | Dafny 2024 | 2024-01-14 |
Presents a concrete method for stabilizing Dafny type-soundness proofs by making the safety predicate and then the typechecker opaque, proving small safety… | ||
| Denotational Recurrence Extraction for Amortized Analysis | ICFP 2020 | 2020-08-23 |
A language-to-language translation extracts recurrences from a credit-annotated source into a cost-bearing simply-typed lambda calculus, using an affine type… | ||
| nothing matches | ||