Katherine Ye

My work applies techniques for programming language design and domain-specific language design to invent declarative and principled modes of information visualization.

Research

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!

News

Feb. 2019

Excited to be interning at Microsoft Research this summer.

July 2018

Excited to join the DSLDI '18 program committee.

April 2018

This summer, Dor Ma'ayan and Lily Shellhammer will be joining the Penrose team, and Nimo Ni will be returning. Welcome!

Mar. 2018

New publication in the Distill journal on the building blocks of interpretability.

Dec. 2017

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

April 2017

This summer, Nimo Ni will be joining the Penrose team 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.

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.

Journal papers

The building blocks of interpretability | NYTimes article
Chris Olah, Arvind Satyanarayan, Ian Johnson, Shan Carter, Ludwig Schubert, Katherine Ye, and Alexander Mordvintsev.
In Distill.

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.

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

I maintain this collection of quotes on notations.