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
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.
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).
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?”
Proofs about programs, proofs as programs, programs as proofs!
Lightning talk on proving code “equal” in Coq.