What is the relationship between Realizability and the Curry-Howard isomorphism?

322 Views Asked by At

I have recently been studying the Curry-Howard isomorphism/correspondence. My sources have primarly been Sørensen [1] and Girard [2]. Realizability is introduced here in the form of Kleene's realizability and (mostly) Kreisel's modified realizability: in this sense, realizability seemed to me simply as the "concrete step" in the application of the Curry-Howard isomorphism.

Stumbling upon the references in [1], I came across J. Van Oosten's "Realizability: a historical essay" [3]. Here little stress was put on the work by Curry, Howard or Kreisel. Girard's (and Krivine's) work is just quickly mentioned.

I thought of two possible answers to my question (not necessarily mutually exclusive):

  1. Realizability is (historically) a predecessor of the Curry-Howard isomorphism, and it has been superseeded by it.

  2. Realizability is a broader approach, and the Curry-Howard isomorphism refers to the results obtained in proof theory by such approach.

[1] Sørensen, Morten Heine, and Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism. Vol. 149. Elsevier, 2006.

[2] Girard, Jean-Yves. Proofs and types. Vol. 7. Cambridge: Cambridge University Press, 1989.

[3] Van Oosten, Jaap. "Realizability: a historical essay." Mathematical Structures in Computer Science 12.03 (2002): 239-263.