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.

Analogies in other fields

Think about the following diagram and related it to Curry-Howard-Lambek correspondence.

Hermeneutic circle(Q1570095) is the recursive structure that represent the iterative nature of interpretation.

Note the three stages in the following diagram:

1. Configuration
2. Refiguration
3. Prefiguration

An Anectodal Reference

Bob Coeche talking about his encounter with Lambeck