4 papers · 1 filter
Compilation as Multi-Language Semantics
William J. Bowman
Modeling interoperability between programs in different languages is a key problem when modeling verified and secure compilation, which has been successfully addressed using multi-…
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…