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

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.

• You might be interested in this paper. – gallais May 12 '16 at 12:10
• This seems to me yet another approach, maybe related to Krivine's (whom I mentioned in my question, but is the one I'm less familiar with). I am inclined to answer myself that the main point is that realizability lies in the realms of semantics, whereas the Curry-Howard isomorphism is a specific result in proof theory. – Matteo May 18 '16 at 17:54
• Well Kleene's realizability was explicitly an effort to formalize the BHK interpretation of intuitionistic logic in the case of Heyting arithmetic. The BHK interpretation is very much wrapped up in Curry-Howard. – Malice Vidrine Jun 22 '16 at 15:59