Useful Links

• The nLab: A category theory wiki.
• Quiver: a tool for drawing commutative diagrams. (Or any diagrams made of arrows!)
• Circuit Simulator
  • This tool taught me a lot when I was younger.
• Digital Library of Mathematical Functions

Papers I Like

Research Interests

• Homotopy Type Theory: Univalent Foundations of Mathematics (many authors)
• Synthetic Differential Geometry, Synthetic Geometry of Manifolds (Kock)
• A General Nullstellensatz for Generalized Spaces (Blechschmidt)
• Using the internal language of toposes in algebraic geometry (Blechschmidt)

Just for Fun

• Sound and Complete Bidirectional Typechecking for Higher-Rank Polymorphism with Existentials and Indexed Types (Dunfield, Krishnaswami)
  • This is basically a complete programming language, with a type system in some ways more powerful than Haskell's, fully specified and proven correct, all in a single paper!
• A Typed, Algebraic Approach to Parsing (Krishnaswami, Yallop)
  • What if we use parser combinators, but don't throw out all of parsing theory?
• Kerr Geodesics in Terms of Weierstrass Elliptic Functions (Cieślik, Hackmann, Mach)
  • Derivation of trajectories around a spinning black hole. (For the non-spinning case, see Wikipedia.)