The “facets of realizability” workshop will take place in Cachan (near Paris) from 1st to 3rd of July 2019. The goal of this workshop is to bring together researchers interested in realizability or whose research involves applications of realizability. Here, “realizability” is to be understood in a very broad sense to foster new ideas from interaction of people working on its different aspects.
Realizability was invented by Kleene in 1945 as an interpretation of arithmetical proofs by numbers encoding recursive functions. In 1952, Kleene extended it to an interpretation of intuitionistic analysis with his second algebra that manipulates elements of the Baire space. These two realizability interpretations, arithmetic realizability and function realizability, can be embedded in the general framework of categorical realizability, a topic that finds its roots in Hyland’s pioneering work in 1982.
Arithmetic and function realizability have different applications. Arithmetic realizability has developed into many variants (Kleene’s number realizability, Kreisel’s modified realizability, Gödel’s Dialectica interpretation, Krivine’s classical realizability) and independence results have been obtained by seeing arithmetic realizability as an extension of forcing. Function realizability has applications in constructive analysis and synthetic topology. Furthermore, computable analysis can be understood to derive from function realizability as it is mostly concerned with the investigation of its computable fragment.
An example of a concept that lies at the border between arithmetic and function realizability is the principle of bar induction. This principle underlies the bar recursion operator that is widely used in arithmetic realizability, but bar induction also relies on the notion of choice sequences, a concept that is ubiquitous in function realizability. The goal of this workshop is to bring together researchers whose interests involve applications of arithmetic, function and categorical realizability to foster new ideas.