I’m a PhD student in the POPV research group at Boston University, co-advised by Ankush Das and Marco Gaboardi. I develop type systems to guarantee behavioral soundness while easing the need/complexity of directly mechanizing code.