The first austral variant of the « Realizability in Chambéry » workshop will take place between the 19th of July and the 23rd of July in the Argentino Hotel in Piriápolis, 100 km east from Montevideo, Uruguay. As for its savoyard counterpart, the mindset is intended to be quite open, but because of the location, it is probably more difficult for you just to pass by.
This meeting will happen as a Boreal Summer School (i.e. Austral Winter) with courses on various topics around realizability in the morning, as well as presentations submitted by the attendants in the afternoon. You are warmly encouraged to submit talks for the afternoon session!
The program is still to be precisely defined. Courses will be given by:
We have a few talk proposals by participants:
There are two possible computational interpretations of second-order arithmetic: Girard's system F and Spector's bar recursion. While the logic is the same, the computational content of these interpretations is very different and their relationship is still to be studied. We make a first step towards a comparison by defining a translation of system F into a simply-typed total language with bar recursion, relying on a realizability interpretation of second-order arithmetic. Because of Gödel's incompleteness theorem there is no proof of termination of system F within second-order arithmetic. However, for each individual term of system F there exists a proof in second-order arithmetic that it terminates, the realizability interpretation of which provides a bound on the number of reduction steps for reaching a normal form. Then, we use this bound to compute the normal form through primitive recursion. Since the normalization proof of system F proceeds by induction on typing derivations, the translation is moreover compositional. Our translation is a first attempt to provide an alternative approach to the study of polymorphism: through bar recursion. The version presented here is a proof of concept that is very flexible and we believe that the technique can be tailored so as to provide a more direct translation, giving new insights on concepts related to polymorphism.
We explain Streicher's construction of categorical models of classical realizability in terms of a change of the structure in an implicative algebra with a closure operator. We show how to perform a similar construction using another closure operator that produces a different categorical model that has the advantage of being —at a difference with Streicher's construction— an implicative algebra.
We propose the new concept of Krivine ordered combinatory algebra (K OCA) as foundation for the categorical study of Krivine’s classical realizability, as initiated by Streicher. We show that K OCA’s are equivalent to Streicher’s abstract Krivine structures for the purpose of modeling higher-order logic, in the precise sense that they give rise to the same class of triposes. The difference between the two representations is that the elements of a K OCA play both the role of truth values and realizers, whereas truth values are sets of realizers in AKSs. To conclude, we give a direct presentation of the realizability interpretation of a higher order language in a K OCA, which showcases the fact that the elements of the K OCA play at the same time the role of programs, and of truth values.
In Krivine classical realizability, one can understand the truth value of a formula (that is the set of its realizers) as its defenders, and the falsity value as the set of its opponents. Following this intuition, the execution of a process is a match between both players, that a realizer should win.
In this talk, we will explain how to use a notion of game to give a precise specification of the realizers of a given formula. We will focus on the particular case of arithmetical formulae, for which our definition relies on the principle of Coquand's games. In the end, we obtain an equivalence between universal realizers and winning strategies (even in presence of non-substitutive instructions such as Quote), which also directly implies the absoluteness of arithmetical formulae for classical realizability.
One common approach to formal compiler construction is to first write the compiler, having in mind in that process the semantics of the involved languages, and then, as a second step, perform the proof of correctness of that compiler. This approach is known as externalist and has been investigated in different formal settings such as formal specification methods (in particular algebraic ones), categorical formalisations of programming languages, dependently-typed languages, etc. In this talk, we present preliminary results of on-going work on an alternative approach to compiler construction that follows an internalist discipline. This means that we develop simultaneously the compiler and its correctness proof. Our development is performed in Agda. The idea is to decorate the data types that model the abstract syntax of each language with the semantics description of that language and write the compiler between those decorated types. That way, compiler correctness reduces to type-correctness. Modulo minor details, the texts of the compiler and its proof are almost the same. We show the translation between a simple while language and a semi-structured code for a stack machine. Although we do not use that framework, our approach has similarities with McBride 's Ornaments.
Current list of known participants:
We have a reasonable amount of funding for people, both for accomodation and trip expenditures. Please manifest yourself quickly if you need funding.
To register, please send a mail with subject tag
[Montevideo2016] to Pierre-Marie Pédrot with your name, affiliation and request for funding.
Send your talk proposals the very same way.
We need to organize that one!