Stephanie Weirich
where else to find them
what they talk about
all 6 in the filters
where they keep going back
all 8 in the filters
on a stage with
all 15 in the filters
who talks about the same things
- Yiyun Liu5 talks
- Nicolas Tabareau14 talks
- Richard A. Eisenberg18 talks
- Max S. New8 talks
- Jonathan Aldrich17 talks
- Steve Zdancewic19 talks
| title | conference | date |
|---|---|---|
| Functional / Logic Programming in Verse | LOPSTR+PPDP 2026 | 2026-08-27 |
Verse claims a tight integration of functional and logic programming with a working prototype and a fresh denotational story: choices and failures are… | ||
| Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach | POPL 2026 | 2026-01-11 |
Shows that reduce-and-compare becomes decidable again with surjective pairing by restricting transitivity to a syntactically defined SN good set of strongly… | ||
| 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… | ||
| Rebound: Efficient, expressive, and well-scoped binding | Haskell 2025 | 2025-10-16 |
Rebound provides well-scoped Haskell term representations using first-class environments that map variables into a fresh scope and statically track scope… | ||
| Consistency of a Dependent Calculus of Indistinguishability | POPL 2025 | 2025-01-19 |
Defines a concrete instance DCOIω with an infinite predicative universe hierarchy and proves logical consistency, strong normalization, and that type… | ||
| Effects and Coeffects in Call-By-Push-Value | OOPSLA 2024 | 2024-10-20 |
Presents a type system for call-by-push-value that statically bounds both observable effects and environmental demands and proves effect-and-coeffect soundness… | ||
| Internalizing Indistinguishability with Dependent Types | POPL 2024 | 2024-01-14 |
DCOI (Dependent Calculus of Indistinguishability) internalizes indistinguishability as definitional equality and adds an observer-indexed identity type so… | ||
| Dependently-Typed Programming with Logical Equality Reflection | ICFP 2023 | 2023-09-04 |
System DE is an explicitly typed core calculus that separates a terminating logical fragment from a potentially diverging programmatic fragment using modes for… | ||
| Program Adverbs and Tlon Embeddings | ICFP 2022 | 2022-09-11 |
Proposes program adverbs as reified functor classes (applicative/selective/monad) that embed effects LiftA2 and Embed constructors to capture static vs dynamic… | ||
| A Graded Dependent Type System with a Usage-Aware Semantics | POPL 2021 | 2021-01-17 |
Presents Grad, a dependent type calculus with natural-number grades and separate demand contexts for terms and types, plus a heap-based reduction using graded… | ||
| Dependent Types in Haskell | Strange Loop 2017 | 2017-09-28 |
Claims that GHC can host useful dependent‑style programming and shows a working library that parses regexes into a compile‑time occurrence map, uses Template… | ||
| Keynote: Dependently-Typed Haskell | Typelevel Summit Philadelphia 2016 | 2016-03-02 |
Argues that Haskell already supports a useful form of dependent typing using GHC features and demonstrates it by encoding red‑black trees with checked… | ||
| Depending on Types | Code Mesh 2015 | 2015-11-03 |
Argues that Haskell already supports a lot of dependently typed programming by using GADTs, datatype promotion and type families to encode invariants… | ||
| nothing matches | ||