• Cornell University
  • Computer and Information Science
  • mail [at] janpaul [dot] pl


I’m a Senior (applying to Doctoral Programs!) at Cornell University working towards degrees in Computer Science with a concentration in Programming Languages & Philosophy with a concentration in Logic advised by Dr. Harold T. Hodes.

My main research interests involve developing practical tools for program verification and theorem proving using both formal & lightweight methods.


This summer, I’m working with Dr. Alwyn Goodloe at the Langley Formal Methods research program at NASA. We’re mechanizing proofs that model correct behaviors behind a Delay-Tolerant Network for NASA’s Interplanetary Overlay Network framework.

Before that, I worked under Dr. Jonathan Aldrich at CMU thanks to the REUSE program. We developed a Gradual Verifier which serves to bridge the gap between static and dynamic verification, by allowing incremental verification of a program. I’ve worked on the first ever gradual verification tool – Gradual C0 – and gradual verification in blockchain programming languages.

And even before that, I started doing Computer Science research under Dr. Adrian Sampson in the Calyx project. We studied optimizations and extensions towards a compiler infrastructure to simplify encoding of high-level program semantics to lower-level synthesizable hardware designs.


Outside of Cornell, I’m part of the Audio/Visual team for SIGPLAN conferences. While this is just volunteering work, I’ve come to put a considerable amount of time into it, so please check out the SIGPLAN YouTube Channel if you’re interested in some cool PL videos!

Idea of a Certain Cat 2004 -Tokuhiro Kawai (川井徳寛)