Abstract:
This thesis reviews several challenges in the use and implementation of faceted execution, a programming-language mechanism for enforcing privacy policies. I present a proof-of-concept of a module-rewriting technique for correctly handling mutable state in Racets, an existing implementation of faceted execution in Racket, and I discuss how static typing and abstract interpretation could improve the safety and efficiency of faceted code.