![](https://janpaul.pl/assets/img/headshot.png)
- Cornell University
- Computer and Information Science
- mail [at] janpaul [dot] pl
About
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 interest involves developing practical frameworks for program verification by creating a set of canonical and reusable representations for domain-specific programs to ease the need to directly mechanize code with automated theorem provers. You can find my research statement here!
Research
This summer, Iβm working with Dr. Alwyn Goodloe at the Langley Formal Methods research program at NASA. Weβre mechanizing proofs with Coq that model correct behaviors behind a well-typed implementation of a Software Defined Delay-Tolerant Networkβs Match-Action pipeline algorithm for NASAβs Interplanetary Overlay Network framework. The well-typedness of the algorithm comes from it being implemented in our NetQIR DSL.
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.
Community
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!
![](assets/img/Tokuhiro_Kawai.jpg)