Katherine Ye

I'm a second-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

I'm interested in designing representations and creative interfaces. I'm particularly interested in the interface between language and image.


I'm co-advised by Keenan Crane and Jonathan Aldrich, in collaboration with Josh Sunshine. We're building a system called Penrose for declaratively and automatically creating semantics-driven visualizations, starting with the domain of mathematics. Check out the Penrose site for more information.

Interested in collaborating, contributing, or using Penrose? Get in touch!


Dec. 2017
Princeton University covered our CCS '17 paper on verifying pseudorandom generators.

Nov. 2017
Excited to join the Arts and AI panel at the MIT Hacking Arts conference.

Aug. 2017
I co-organized an experimental event called an antidisciplinarathon. Here's what happened.

June 2017
I gave a talk at Y Conf, a conference at Y Combinator Research.

May 2017
PROCESS II is out! It's a zine on creative processes, made in collaboration with many contributors from diverse disciplines.

April 2017
Nimo Ni will be joining Penrose this summer as an REU intern. Welcome!

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

Feb. 2016

Conference papers

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.

Workshop papers

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

Technical reports

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.


PROCESS: finding desire paths in creative interfaces
Y Conf 2017, hosted by Y Combinator Research
An experimental talk exploring pieces from the zine PROCESS II and ways they suggest improving interfaces to support creative processes.

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.

Other work

Here's some more work.

I maintain this collection of quotes on notations.
You can follow me on Twitter or hear about my work via email.