Publications

Joshua M. Cohen and Philip JohnsonFreyd. A Formalization of Core Why3 in Coq. POPL 2024: 51st ACM SIGPLAN Symposium on Principles of Programming Languages, January 2024. doi pdf code slides

Joshua M. Cohen and Andrew W. Appel. Specifying and Verifying a RealWorld Packet ErrorCorrection System. VSTTE 2023: 15th International Conference on Verified Software: Theories, Tools, and Experiments, October 2023. pdf code slides

Joshua M. Cohen, Qinshi Wang, and Andrew W. Appel. Verified Erasure Correction in Coq with MathComp and VST. CAV 2022: 34th International Conference on ComputerAided Verification, August 2022. doi pdf code slides

Joachim Breitner, Antal SpectorZabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua Cohen, and Stephanie Weirich. Ready, Set, Verify! Applying Hstocoq to Realworld Haskell Code. Journal of Functional Programming, 31:140, February 2021. doi
Unpublished Drafts

Joshua M. Cohen and Andrew W. Appel. Towards Practical Verification of LargeScale Numerical Software Libraries. 2024. pdf
Talks

Towards a Verified Intermediate Verification Language. IFIP Working Group 2.3 Programming Methodology. May 2024.

A Formalization of Core Why3 in Coq. New Jersey Programming Languages and Systems Seminar. May 2023.

Verified Erasure Correction in Coq with MathComp and VST. New Jersey Programming Languages and Systems Seminar. May 2022.
Service

ICFP 2024 Artifact Evaluation Committee
Teaching

Teaching assistant for COS 510: Programming Languages, Princeton University, Spring 2023

Teaching assistant for COS 423: Theory of Algorithms, Princeton University, Fall 2022

Teaching assistant for CIS 320: Introduction to Algorithms, University of Pennsylvania, Spring 2020, Fall 2019

Teaching assistant for CIS 120: Programming Languages and Techniques, University of Pennsylvania, Spring 2019, Fall 2018, Spring 2018