Katherine Ye

I'm a first-year PhD student in 💻✨ at Carnegie Mellon University.

My work is supported by a Google Anita Borg Memorial Scholarship and an ARCS Foundation Fellowship.

Smith (EDSH) 232


Feb. 2017—I'm excited to be interning at Google Brain on the Distill team this summer!

I work on creating powerful representations in the form of languages and visualizations and on redesigning creative interfaces to reify second-order creativity.

Current work

I'm co-advised by Keenan Crane and Jonathan Aldrich, in collaboration with Josh Sunshine. We are building a system called Penrose to automatically visualize mathematics. For more information, see the extended remix of the talk I gave at Off the Beaten Track '17 and the talk proposal. You can also join the mailing list.

Interested in collaborating or contributing, or have suggestions based on your diagramming workflow? Get in touch!

Conference papers

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).
Appearing at 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.

Workshop papers

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).

Unpublished work

The Notorious PRG: Formal verification of the HMAC-DRBG pseudorandom number generator
Senior thesis. Paper in progress.
Advised by Andrew W. Appel and Matt 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.


Designing extensible, domain-specific languages for mathematical diagrams
Off the Beaten Track 2017
Talk accompanying the OBT proposal. Here's the extended remix I gave at PLunch.

Strange loops: powerful knot notations
Strange Loop 2015
Reviewed by Philip Wadler: “In my series of favourites from Strange Loop 2015 (...) Great fun for anyone interested in how to describe complex situations, and which programming language aficionado can resist that?”

Proof assistants as a tool for thought
Tools for Thought workshop, hosted by the Recurse Center, 2016
Overview of the workshop by Shriram Krishnamurthi.

Proofs about programs, proofs as programs, programs as proofs!
!!con 2014
Lightning talk on proving code “equal” in Coq.


I maintain this collection of quotes on interesting notations.
Here's a portfolio of some other outputs.
I'm also on Twitter.