- Cornell University
- Analytic Philosophy and Type Theory
- 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
Iβm currenty working with Dr. Alwyn Goodloe at NASAβs Langley Formal Methods. Weβre mechanizing proofs with Coq that model correct behaviors behind a well-behaved implementation of a Software Defined Delay-Tolerant Networkβs Match-Action pipeline algorithm for NASAβs Interplanetary Overlay Network framework. The well-behavedness of the algorithm comes from it being implemented in our networks DSL: NetQIR !
Iβm also working with Dr. Adrian Sampson on the Calyx project. Here, Iβm figuring out how to model hardware-level parallelism using Kleene Algebra with Tests.
In addition, Iβm a 2Γ CMU REUSE alumni. I worked under Dr. Jonathan Aldrich in developing a Gradual Verifier, seeking to bridge the gap between static and dynamic verification. I worked on the first ever gradual verification tool β Gradual C0 β and made use of gradual verification for blockchain programming languages.
Community
Iβm a member 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 feel free check out SIGPLANβs official YouTube Channel if youβre interested in some cool PL videos!
Tired of my site? Click here for a random one of my friends.