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


I’m a Junior 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 excited to work with Dr. Alwyn Goodloe in the Langley Formal Methods research program at NASA. We’ll be using Coq to formally verify theorems proving the soundness of network protocols.

Since before that, I’ve been working under Dr. Jonathan Aldrich at CMU thanks to the REUSE program. We are developing 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 (川井徳寛)