12 citations · 16 across the 5 of their papers we have counts for
5 papers
Dependent-Type-Preserving Memory Allocation
Paulette Koronkevich, William J. Bowman
Dependently typed programming languages such as Coq, Agda, Idris, and F*, allow programmers to write detailed specifications of their programs and prove their programs meet these s…
One Weird Trick to Untie Landin's Knot
Paulette Koronkevich, William J. Bowman
In this work, we explore Landin's Knot, which is understood as a pattern for encoding general recursion, including non-termination, that is possible after adding higher-order refer…
Type Universes as Allocation Effects
Paulette Koronkevich, William J. Bowman
In this paper, we explore a connection between type universes and memory allocation. Type universe hierarchies are used in dependent type theories to ensure consistency, by forbidd…
PLIERS: A Process that Integrates User-Centered Methods into Programming Language Design
Michael Coblenz, Gauri Kambhatla, Paulette Koronkevich +5
Programming language design requires making many usability-related design decisions. However, existing HCI methods can be impractical to apply to programming languages: they have h…
Obsidian: Typestate and Assets for Safer Blockchain Programming
Michael Coblenz, Reed Oei, Tyler Etzel +6
Blockchain platforms are coming into broad use for processing critical transactions among participants who have not established mutual trust. Many blockchains are programmable, sup…