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?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.