Katherine Ye

I'm interested in designing powerful representations and creative interfaces.

News

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

I'm honored to be awarded the Computing Research Association (CRA) Outstanding Undergraduate Researcher Award.

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

Verified correctness and security of mbedTLS HMAC-DRBG
Katherine Ye, Matthew Green, Naphat Sanguansin, Lennart Beringer, Adam Petcher, and Andrew W. Appel.
To appear in 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. (* joint first authors)
In submission.

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.

Talks

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

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