|
|
|
|
|
|
by lou1306
2988 days ago
|
|
|
> Further topics to explore: the BHK interpretation of intuitionistic proof and the univalence axiom in homotopy type theory. Thanks! For the interested, Girard's book focuses on the Curry-Howard isomorphism, another great result linking computer programs (actually, the typed lambda-calculus) to mathematical proofs. |
|
|