About Me

I am a CS PhD student at CMU working under Jan Hoffmann in the area of programming languages. Right now I'm working with Resource Aware ML, and am looking at the surrounding area of quantitative type theory.


Research Interests

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.


    Contact

    davidkah at cs dot cmu dot edu

    GHC 6503