Specification and verification for functional and imperative programs

Vikramaditya Singh


Engineering and Applied Sciences

Project Summary

This summer I had the opportunity to work with the Department of Computer Science, and specifically the DeepSpec project. The DeepSpec project conducts research on how the correctness of software and hardware should be specified and verified. Within the broader DeepSpec project, I worked with Professor Stephanie Weirich, PhD candidate Yao Li, and fellow PURM researcher Mohamed Abaker on the hs-to-coq project.

Haskell (hs) is a functional programming language widely used in both academia and industry. On the other hand, Coq is another programming language that is used as a proof assistant to prove/verify theorems about mathematics and software programs. Hs-to-coq is a tool developed at UPenn that transpiles Haskell code into Coq so that Haskell programs can be verified. I spent my summer using Coq to specify and verify Haskell’s IntMap data structure as a proof-of-concept for hs-to-coq, and to prove the correctness of the data structure.

In order to begin working on the Coq proofs of IntMap, Mohamed and I, along with other PURM researchers working with the DeepSpec project, underwent a two-week crash course on Coq after which Mohamed and I did further research that was more specific to our project. However, when we began attempting proofs, we often had to turn to Professor Weirich, Yao, and UPenn’s Programming Language Club to understand the existing proofs and figure out how to complete tricky parts of our own proofs. Over the course of the summer, we were able to work more independently and complete more complex proofs on our own.

Being part of the research project taught me a lot about software verification, as well as the nature of academic research. I gained technical skills and knowledge on Coq, the IntMap data structure, and Emacs (the text editor used to write Coq code). As well as that, I better understood the dynamics of academic research through attending professional development seminars and talks hosted by the Programming Language club. Finally, I gained further experience in using academic tools such as Git/GitHub, Slack, and virtual conferencing software. I am grateful for the exposure to Computer Science research at UPenn, and look forward to making further contributions to this project in the future.