Jonathan Aldrich
where else to find them
no profile links on file
what they talk about
all 9 in the filters
where they keep going back
all 8 in the filters
on a stage with
all 23 in the filters
who talks about the same things
- Frank Pfenning6 talks
- Joshua Sunshine3 talks
- Ondřej Lhoták11 talks
- Ranjit Jhala19 talks
- Benjamin Delaware18 talks
- Amal Ahmed25 talks
| title | conference | date |
|---|---|---|
| Security Reasoning via Substructural Dependency Tracking | POPL 2026 | 2026-01-11 |
A new type system flips substructural resource reasoning from inputs to outputs and implements a suspended computation connective so effects are produced when… | ||
| Structural Information Flow: A Fresh Look at Types for Non-Interference | OOPSLA 2025 | 2025-10-16 |
Type system separates data abstraction from information flow, turns single labels into dependency sets, and encodes quantifiers as existentials so module… | ||
| Unfolding Expressions for Gradual Verification | IWACO 2025 | 2025-10-14 |
Formalizes evaluation and proof obligations for unfolding expressions in gradual verification, giving both static (isorecursive) and dynamic (equirecursive)… | ||
| Usability Barriers for Liquid Types (Summary of Published Work) | HATRA 2025 | 2025-10-14 |
Study of 19 developers (12 new to LiquidHaskell, 7 experienced) identifies nine concrete barriers across three themes: verification, developer experience, and… | ||
| Gradual Verification: Assuring Software Incrementally | IWACO 2025 | 2025-10-14 |
Proposes gradual verification that lets each assertion be complete, partial, or omitted and gives a sound mix of static and runtime checks so every spec… | ||
| Usability Barriers for Liquid Types | PLDI 2025 | 2025-06-16 |
Study reports a user study of LiquidHaskell with 12 novice and several experienced participants, yielding nine barriers across three concrete categories… | ||
| The Meerkat Vision: Language Support for Live, Scalable, Reactive Web Apps | Onward! 2024 | 2024-10-23 |
Meerkat presents a language that implements live code and data updates with atomic reconfiguration so UI, state and actions change together; the prototype runs… | ||
| Substructural Information Flow via Polymorphism | IWACO 2024 | 2024-10-21 |
Argues that information flow is expressible with parametric polymorphism replaces lattices, presents a prototype type system implemented in OKL/OCaml tooling… | ||
| Gradual Verification for Smart Contracts | PriSC 2024 | 2024-01-20 |
Gradual verification combines static separation-logic proofs with imprecise specifications (written as question marks) and automatically emits dynamic checks… | ||
| Sound Gradual Verification with Symbolic Execution | POPL 2024 | 2024-01-14 |
Provides a formal, machine-checked semantics for symbolic execution and for optimized runtime-check generation, proves that gradual verification implemented… | ||
| Latte: Lightweight Aliasing Tracking for Java | IWACO 2023 | 2023-10-24 |
A formal alias-tracking type system for Java that requires annotations only on parameters and fields, infers all local aliases, and enforces unique parameters… | ||
| Latte: Lightweight Aliasing Tracking for Java | HATRA 2023 | 2023-10-22 |
Latte adds a lightweight aliasing layer to Java that only requires annotations on parameters and fields while inferring local variable annotations, tracks… | ||
| Static Information Flow Control Made Simple | HATRA 2022 | 2022-12-05 |
Proposes a rule-based IFC that unifies confidentiality and integrity by declaring concrete flows between modules, using overrides via lexical scope to allow… | ||
| A Case Study in Language-Based Security: Building an I/O Library for Wyvern | SPLASH 2022 | 2022-12-05 |
Builds a small standard I/O library for Wyvern that combines object capabilities, an effect system, and language extensions to reduce misuse. Demonstrates… | ||
| Gradual Verification of Recursive Heap Data Structures | OOPSLA 2020 | 2020-11-15 |
Practical system that extends a base static verifier with gradual formulas and optimistic strengthening, inserting runtime checks when a missing spec was… | ||
| A Case Study in Language-Based Security: Building an I/O Library for Wyvern | Onward! 2020 | 2020-11-15 |
A small standard I/O library for Wyvern is built and shown workable: capabilities enforce least privilege by handing narrow file or directory handles… | ||
| An Empirical Study of Ownership, Assets, and Typestate in Obsidian | OOPSLA 2020 | 2020-11-15 |
A new language, Obsidian, implements typestate and linearity to track ownership and prevent asset loss; authors run a randomized controlled trial with 20… | ||
| nothing matches | ||