Joshua Cohen


I'm a 3rd year PhD student, advised by Andrew Appel. My research interests include formal verification, proof assistants, algorithms, and functional programming. Currently, I am working on verifying network components written in C using Coq and the Verified Software Toolchain.

I recieved my BA in math and computer science and my MSE in computer science from the University of Pennsylvania in 2020. During my undergrad, I worked with Stephanie Weirich on verifying Haskell code in Coq using hs-to-coq and with Sanjeev Khanna on distributed graph algorithms.

Since summer 2022, I have interned at Sandia National Labs, where I am working on formal semantics for the Why3 intermediate verification language.

In summer 2021, I was an Applied Scientist Intern with the AWS Identity Automated Reasoning Group, where I used Dafny to verify parts of the IAM policy evaluator.