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
kqy@cs.cmu.edu
CV

My work focuses on designing intelligent interfaces that augment human visual cognition and creation. To do that, I study and create powerful representations.

News

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

Research

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

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 papers

Verified correctness and security of mbedTLS HMAC-DRBG
Katherine Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, and Andrew W. Appel.
In submission.

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.

Talks

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 a portfolio of art-related work.

I maintain this collection of quotes on notations.
I'm also on Twitter.