I began a PhD program at MIT in computer science (specifically programming languages) in the fall of 2013. I majored in mathematics and physics as an undergrad at MIT. I'm especially interested in category theory, homotopy type theory, interactive proof assistants, general relativity, quantum mechanics, topology, and education. I've been working on developing a category theory library in Coq with David Spivak and Adam Chlipala, with an eye towards applications to databases.
- Stack Overflow 5.4k 5.4k 11 gold badge2222 silver badges5353 bronze badges
- TeX - LaTeX 2k 2k 1515 silver badges2626 bronze badges
- MathOverflow 643 643 11 gold badge77 silver badges1616 bronze badges
- Mathematica 569 569 22 silver badges1010 bronze badges
- Theoretical Computer Science 251 251 11 silver badge55 bronze badges
- View network profile
Top network posts
- 40 Formalizations of category theory in proof assistants
- 20 How do I make an attached file display like a link?
- 19 std::cout equivalent at compile time, or static_assert stringification of compile-time constant values in c++11
- 18 How do we construct the Gödel’s sentence in Martin-Löf type theory?
- 18 Formalizations of category theory in proof assistants
- 16 Dividing dimensions to get a count
- 15 Removing brackets from biblatex references for lncs
- View more network posts →