4 papers
Verifying Provenance of Digital Media: Why the C2PA Specifications Fall Short
Enis Golaszewski, Neal Krawetz, Alan T. Sherman +8
The rapid rise of generative AI has made it easy to create convincing fake media at scale. In response, an industrial coalition has developed the Coalition for Content Provenance a…
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…