Logics for computability

His motivation was to make precise the Heyting–Brouwer–Kolmogorov (BHK) interpretation of intuitionism, according to which proofs of mathematical statements are to be viewed as constructive procedures.

Kleene's original realizability interpretation has received much attention among those who study connections between computability and logic.

It was extended to full higher-order intuitionistic logic by Martin Hyland in 1982, who constructed the effective topos.

In 2002, Steve Awodey, Lars Birkedal, and Dana Scott formulated a modal logic for computability, which extended the usual realizability interpretation with two modal operators expressing the notion of being "computably true".

Such a semantics sees games as formal equivalents of interactive computational problems, and their "truth" as existence of algorithmic winning strategies.