Difference between revisions of "Curry-Howard-Lambek correspondence"
Jump to navigation
Jump to search
Line 1: | Line 1: | ||
{{WikiEntry|key=Curry-Howard-Lambek correspondence|qCode=110810925}} | {{WikiEntry|key=Curry-Howard-Lambek correspondence|qCode=110810925}} 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 relation]]s, as a self-sufficient environment for software verification and validation cycle. | |||
[[Category:Category Theory]] | [[Category:Category Theory]] |
Revision as of 09:01, 21 February 2022
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.