Curry-Howard-Lambek correspondence

Curry-Howard-Lambek correspondence(Q110810925) is an extension of Curry-Howard correspondence.

By thinking about the correspondence between Proof, Programs, and Categories, we can see a circular triangle of data types that mutually serves and the Test Assertions, Proposed Programs, and Data Content in ordered relations, as a self-sufficient environment for software verification and validation cycle.