In Wikipedia we can read that
the Curry–Howard correspondence is a correspondence between formal proof calculi and type systems for models of computation. In particular, it splits into two correspondences. One at the level of formulas and types that is independent of which particular proof system or model of computation is considered, and one at the level of proofs and programs which, this time, is specific to the particular choice of proof system and model of computation considered.
In this other related question I asked about the relation between the C-H correspondence as it was conceived and quantum computing. Here the questions are:
- Does this theory have to be updated to embrace quantum-specific phenomena like extended causality?
- If yes, what are the changes made?
