Research

Thinking Outside the □: Verified Compilation of ML5 to JavaScript.1 Senior thesis, 2017. Advisor: Daniel R. Licata.
[pdf] [poster] [Agda code]

Intrinsic Verification of a Regular Expression Matcher. With Maksim Trifunovski and Daniel R. Licata. Submitted, 2016.
[pdf] [Agda code]



  1. Read the symbol □ as “box”.