About Me

I am a CS PhD student at CMU working under Jan Hoffmann in the area of programming languages. I work on a type system that allows for automatic cost analysis, called Automatic Amortized Resource Analysis (AARA). Just code as usual, and the type system will tell you how much time, or space, or energy, etc. the program will use as a function of its input. You can find an implementation of it as Resource Aware ML.


Research Interests

Right now my main focus is in cost analysis, but in general I am interested in designing languages to allow much more utility than usual to be squeezed out. This can come in many shapes:

  • type theory
  • domain-specific languages
  • decision procedures
  • logic
  • proof assistants
  • static analyses

    • Some History

    I started my PhD at CMU in 2018. The summer before that, I worked on Hack at Facebook. And the spring before that, I earned my BS in CS from Cornell, along with Math and Philosophy minors. And before all that, I grew up in a town outside Philadelphia called Eagleville.


    Contact

    davidkah at cs dot cmu dot edu

    GHC 6503