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).
Appearing at 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.
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. Paper in progress.
Advised by Andrew W. Appel and Matt 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.
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.