Robert Harper
where else to find them
no profile links on file
what they talk about
where they keep going back
- POPL3 editions2022–2026
on a stage with
all 5 in the filters
who talks about the same things
- Harrison Grodin3 talks
- Yue Niu2 talks
- Jonathan Sterling4 talks
- Runming Li3 talks
- Jan Hoffmann9 talks
- Lars Birkedal35 talks
| title | conference | date |
|---|---|---|
| Mechanizing Synthetic Tait Computability in Istari | CPP 2026 | 2026-01-12 |
Mechanization of Synthetic Tait Computability is formalized in the Istari extensional type theory with equality reflection, producing a reusable library of… | ||
| Abstraction Functions as Types | POPL 2026 | 2026-01-11 |
Encodes abstraction functions inside types by adding a single new proposition (an abstract phase) to univalent dependent type theory, then uses a gluing… | ||
| Decalf: A Directed, Effectful Cost-Aware Logical Framework | POPL 2024 | 2024-01-14 |
Decalf is a directed, effectful, cost-aware logical framework implemented in Agda that equips every type with an intrinsic preorder so a cost bound can itself… | ||
| A Cost-Aware Logical Framework | POPL 2022 | 2022-01-16 |
Presents calf, a full-spectrum dependent type theory that treats cost as an effect and enforces an internal noninterference property so I/O behavior cannot… | ||
| A metalanguage for multi-phase modularity | ML 2021 | 2021-08-26 |
Proposes a metalanguage that lets the compiler inline representations without breaking programmer abstractions by indexing types and judgments in a phase… | ||
| nothing matches | ||