Realizability for classical logic, concurrency, references and rewriting – RECRE

The goal of this project is to get a better understanding of the proofs-as-programs correspondence for classical logic using the recent advances of the theory of classical realizability.

Currently, this correspondence is very well developed and understood in the case of pure functional programming, without side effects nor control. It has remarkable outputs both on the theoretical and practical sides: rich models of intuitionistic logic and constructive mathematics have been studied, proof assistants and theorem provers have been developed and used to prove significant results, and mathematical models of functional computation have been used for program specification and certification, in particular using the technique of program extraction from mathematical proofs.

Following the discovery by Griffin in 1990 of a correspondence between classical logic and control operators in functional programming, Krivine developed classical realizability as a complete reformulation of the principles of realizability in the context of classical reasoning. At the core is the idea that realizers of a given formula are programs that respect a specification associated with the formula, and that specifications are formulated in terms of the interaction of a program with its environment. Quite surprisingly, this construction can be seen as a generalization of the model theoretic notion of forcing as introduced by Cohen in the 60's to prove independence results in set theory, such as the independence of the continuum hypothesis. Thanks to the theory of classical realizability, such axioms were recently given a computational content in terms of very concrete programming features, including a global clock and memory management primitives. This striking connections naturally suggest new directions to extend the proofs as programs paradigm beyond the scope of functional programming.

The aim of our project is to study and develop this computational interpretation of logic and the technology of classical realizability itself, using the expertise of researchers from several neighboring areas. Indeed, the proofs-as-programs correspondence is intrinsically interdisciplinary since its domains range from mathematical logic to programming language design through category theory and theoretical computer science. We plan to investigate the connections between realizability, forcing and side effects (Task 2) as well as the possible applications of this technology to program extraction (Task 3). We also plan to develop and systematize realizability techniques in concurrent programming and low level languages (Task 4), while studying the algebraic structures underlying realizability using category theory and game semantics (Task 5).