| layout | post |
|---|---|
about |
./_includes/publication.html |
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!
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.
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!
<script> // Define an array of friends' links and their names const friends = [ { name: 'Song', url: 'https://s-ye.github.io/me/' }, { name: 'Inle', url: 'https://imbush.github.io/' }, { name: 'Sid', url: 'https://sholalkere.github.io/' }, { name: 'Ben', url: 'https://camto.github.io/' }, { name: 'Sina', url: 'https://sinearc.github.io/' }, { name: 'Elaine', url: 'https://samoyed.blog/' }, { name: 'Alex', url: 'https://www.eecs.tufts.edu/~abai02/'}, { name: 'John', url: 'https://j-hui.com/'}, { name: 'Chris', url: 'https://flyingrocksquirrel.github.io/'}, { name: 'Max', url: 'https://conf.researchr.org/profile/conf/maxsun'}, { name: 'Espada', url: 'https://x.com/guiespada'} ]; // Function to choose a random friend and return the URL function getRandomFriendURL() { const randomIndex = Math.floor(Math.random() * friends.length); return friends[randomIndex].url; } // Function to handle the link click (normal and middle-click) function handleLinkClick(event) { const randomFriendURL = getRandomFriendURL(); // If middle mouse button is clicked or Ctrl/Command key is pressed, open in a new tab if (event.button === 1 || event.ctrlKey || event.metaKey) { window.open(randomFriendURL, '_blank'); // Open in a new tab } else { // For normal clicks, redirect in the same tab window.location.href = randomFriendURL; } event.preventDefault(); // Prevent default behavior of link } </script>Tired of my site? Click here for a random one of my friends.
