Correspondence between Programs and Proofs (and Categories). https://courses.cs.cornell.edu/cs3110/2021sp/textbook/adv/curry-howard.html https://ncatlab.org/nlab/show/computational+trilogy