David Binder
where else to find them
no profile links on file
what they talk about
all 4 in the filters
where they keep going back
- OOPSLA2 editions2023–2024
all 5 in the filters
on a stage with
all 8 in the filters
who talks about the same things
- Ishan Bhanuka3 talks
- Ondřej Lhoták11 talks
- Andres Löh7 talks
- Philip Wadler14 talks
- Ingo Skupin4 talks
- Stephanie Weirich14 talks
| title | conference | date |
|---|---|---|
| Is There a Future for a Formally Specified Haskell Report | 2026 Haskell Implementors' Workshop | 2026-06-05 |
Project implements a verified frontend in Lean that covers Unicode lexing, indentation-sensitive tokenization, renaming, fixity resolution and grouping of… | ||
| From FP to OOP and Back, Consistently | UNSOUND 2024 | 2024-10-20 |
Extends dependent defunctionalization and refunctionalization to dependent types, proving the transformations are total and type-preserving and giving a… | ||
| Deriving Dependently-Typed OOP from First Principles | OOPSLA 2024 | 2024-10-20 |
Derives a dependently typed object-oriented fragment by duality and gives a concrete calculus with two symmetric language fragments plus type- and… | ||
| Getting into the Flow: Towards Better Type Error Messages for Constraint-Based ... | OOPSLA 2023 | 2023-10-23 |
Proposes turning constraint-generation into explicit data flows by attaching provenances (sequences of source locations) to algebraic subtyping constraints… | ||
| Structural Refinement Types | TyDe 2022 | 2022-09-11 |
A lightweight refinement-type system and inference algorithm extends algebraic subtyping with rules from polymorphic variants to infer precise refinements… | ||
| Introduction and Elimination, Left and Right | ICFP 2022 | 2022-09-11 |
Claims that four rule choices—right/left introduction and elimination—yield four distinct program structures but are equally expressive through mechanical… | ||
| nothing matches | ||