I am in my third year of graduate study in computer science at MIT. My interests include type theory and functional programming and their application to software verification. I’m advised by Adam Chlipala and Mike Carbin.
I am currently studying how to program with topological spaces (such as the real numbers or probability distributions). I’m building a programming language, embedded in Coq, whose types are topological spaces and whose expressions are continuous maps. It’s all based on formal topology, a constructive theory of topology.
I’m also working on a project to use Coq to derive solvers for mathematical optimization problems and inference algorithms for statistical inference problems.