3 papers
cs.PL2025
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…
cs.PL2025
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…
cs.PL2024
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…