A deep correspondence between proofs and programs

Congratulations to Husna Farooqui on the defense of her MA thesis, “The Curry-Howard Correspondence”, on August 6, 2021.

Her committee members included Richard Zach, Nicole Wyatt, and Jeremy Fantl.

We asked Husna to provide us with some insight into her thesis, and her graduate studies experience in the Department of Philosophy at the University of Calgary.

Tell us about your thesis topic.

My thesis is about the Curry-Howard correspondence, which is ordinarily described as a deep correspondence between proofs and programs. In particular, I wrote on the Curry-Howard correspondence between intuitionistic natural deduction and the simply-typed lambda calculus and tried to demonstrate the isomorphism in full. My thesis is meant to be an elementary introduction that also covers some brief history, background knowledge, as well as the significance of the correspondence.

What was the most valuable outcome of the Graduate program for you?

Completing a graduate degree requires a significant amount of work and dedication, so completing the program was a valuable experience for me as I learned about my own capabilities. I also really valued my experience in the program because it provided me the possibility of learning and exploration. All that to say for me, the program was such a learning experience, and this is the thing that I value most.

What are the next steps/plans for you?

The next steps are not entirely clear yet! But I can say that I write this answer from the vibrant city of Toronto, which is my new home for the next little while. For now, I’m hoping to get settled here and continue exploring!