I'm a fifth-year PhD student in 💻✨ at Carnegie Mellon University.
My work is supported by the NSF, a Microsoft Research PhD Fellowship, a Google Anita Borg Memorial Scholarship, and an ARCS Foundation Fellowship.
Office: Smith (EDSH) 232
Penrose-related queries: team@penrose.ink
Other queries: kqy@cs.cmu.edu
Penrose: From Mathematical Notation to Beautiful Diagrams
Katherine Ye, Nimo Ni, Max Krieger, Dor Ma'ayan, Jenna Wise, Jonathan Aldrich, Joshua Sunshine, Keenan Crane
In SIGGRAPH '20.
How domain experts create conceptual diagrams and implications for tool design (Best Paper Honorable Mention)
Dor Ma'ayan*, Nimo Ni*, Katherine Ye, Chinmay Kulkarni, Joshua Sunshine (*equal contribution)
In CHI '20.
Verified correctness and security of mbedTLS HMAC-DRBG | slides
Katherine Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, and Andrew W. Appel.
In ACM CCS '17.
The end of history? Using a proof assistant to replace language design with library
design
Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit
Suriyakarn, Peng Wang and Katherine Ye (alphabetical).
In SNAPL (Summit for Advances in Programming Languages) '17.
Verified correctness and security of OpenSSL HMAC
Lennart Beringer, Adam Petcher, Katherine Ye, and Andrew Appel.
In USENIX Security ’15.
The building blocks of interpretability | NYTimes article
Chris Olah, Arvind Satyanarayan, Ian Johnson, Shan Carter, Ludwig Schubert, Katherine Ye, and Alexander Mordvintsev.
In Distill.
Substance and Style: domain-specific languages for mathematical diagrams
Wode Ni*, Katherine Ye*, Joshua Sunshine, Jonathan Aldrich, and Keenan Crane. (*equal contribution)
In DSLDI '17 (co-located with SPLASH).
Designing extensible, domain-specific
languages for mathematical diagrams
Katherine Ye, Keenan Crane, Jonathan Aldrich, and Joshua Sunshine.
In Off the Beaten Track ’17 (co-located with POPL).
The Notorious PRG: Formal verification of the HMAC-DRBG pseudorandom number generator
Senior thesis.
Advised by Andrew W. Appel and Matthew Green.
Joint work with Adam Petcher, Lennart Beringer, and Naphat Sanguansin.
Testing typed functional programs and re-synthesizing them
Katherine Ye, advised by David Walker. Junior paper.