Showing cs.PLShow all
3 papers · 1 filter
cs.PL2025
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-…
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…