Program

One aim of the theory of realizability toposes is to give a conceptual and semantic account of the various realizability interpretations one can find in the proof-theoretic literature. But there is no direct route which goes from a proof-theoretic interpretation to its “corresponding” topos. In fact, one quickly finds that one has to make some choices on the way. I will discuss some of the issues that come up when one tries to define a modified realizability topos. Recall that the proof theorist (Kreisel, Troelstra) will think of modified realizability as an interpretation of arithmetic in finite types which validates independence of premise and the axiom of choice for all finite types. In the literature (Van Oosten’s book, for instance) one can find a modified realizability topos, due to Grayson, but it does not validate the axiom of choice for all finite types. I will discuss two possible ways in which this can be fixed. If time permits, I may even discuss a fourth topos which also has some claim to being a topos for modified realizability.

In this talk I will present a notion of realizability for bounded nonstandard arithmetic in all finite types as well as variants with q and t-truth. The boundedness comes from using Howard-Bezem majorizability conditions. This notion of realizability and its variants with truth are sound and complete. They also bare some similarities with other notions of realizability. In fact, by restricting to the so-called “purely external fragment” one recovers the bounded modified realizability of Fernando Ferreira and Ana Nunes [5]. Moreover, this notion of realizability also bares similarities with the notion of realizability given by Benno Van den Berg, Eyvind Briseid and Pavol Safarik [1] but replacing finiteness conditions by Howard-Bezem majorizability conditions. I will make a connection with recent work by Paulo Oliva and I on parametrised functional interpretations [4] and finish with some open questions.
(Joint work with Jaime Gaspar [2,3] and Paulo Oliva [4])[1] Benno van den Berg, Eyvind Briseid, and Pavol Safarik. A functional interpretation for non-standard arithmetic. Annals of Pure and Applied Logic, 163(12):1962-1994, 2012.
[2] Bruno Dinis and Jaime Gaspar. Intuitionistic nonstandard bounded modified realisability and functional interpretation. Annals of Pure and Applied Logic 169(5):392-412, 2018.
[3] Bruno Dinis and Jaime Gaspar. Nonstandard interpretations with truth (in preparation).
[4] Bruno Dinis and Paulo Oliva. Parametrised Functional Interpretations (in preparation).
[5] Fernando Ferreira and Ana Nunes. Bounded modified realizability. The Journal of Symbolic Logic, 71(1):329-346, 2006.

In the late seventies William C. Powell generalized the construction of Heyting-valued universes, by considering a generalization of a Heyting Algebra, one that we call a Powell Algebra. The main new class of examples of Powell Algebras, however, is very different from a Heyting Algebra; it is based on the notion of Partial Applicative Structures (PAS). I will present the construction of a P-valued model of Intuitionistic Zermelo Fraenkel Set Theory when P is a Powell Algebra derived from a PAS. The semantics of statements in this model can be described as a natural generalization to set theoretic formulas of Kleene’s 1952 notion of realizability.
Following this, I will discuss in some detail the Realizability Universe, the P-valued model when P is derived from Kleene’s PAS whose underlying set is the set of natural numbers and whose binary operation is induced from the natural number coding of recursive functions. It’s a set theoretic adaptation of Martin Hyland’s Effective Topos. I will use this model to verify a couple of independence results. For example, I will show that the law of excluded middle is independent of the axioms of Intuitionistic Zermelo Fraenkel Set Theory (IZF). I will also use the model to verify a couple of consistency results, e.g. Markov’s Principle and Church’s Thesis.
Strong Church’s Thesis (SCT) is the statement that all functions on the natural numbers are recursive. The final result of this talk is to establish that SCT is true in the Realizability Universe. Since the meta-theory we employ is inuitionistic as well, our result means that SCT+IZF is consistent relative to IZF or in other words, Cons(IZF) implies Cons(IZF + SCT). An obvious advantage of carrying out the construction of our models in an intutionistic meta-theory is that this construction can be repeated inside our new model. The construction of our P-valued models is an iterative operation.

It is a common conception of constructive mathematics that all its objects must be constructed. This separates constructive mathematics from large parts of main stream mathematics where one works predominantly with abstract structures on an axiomatic basis. We argue that this separation is unnecessary, and that it makes perfect sense to study abstract structures from a constructive point of view. Moreover, we show that ‘constructive abstract mathematics’ has concrete computational content – even in the presence of restricted forms of non-constructive reasoning and choice principles.
As a framework for formalizing abstract mathematics we consider first order logic extended by strictly positive inductive or coinductive predicates. The extraction of computational content is based on a version of realizability that treats quantifiers uniformly in order to account for abstract structures whose elements cannot be used in computations.
We give examples from computable analysis to underpin the practical usefulness of our approach.

Working in an arithmetic topos, we introduce an elementary interval structure that allows to axiomatise notions of path as well as path-connectedness on objects. The paths in question are in a sense abstract counterparts of Moore paths in topology. This apparatus paves the way to an abstract version of Hurewicz fibrations and related topological notions like fundamental groupoid, homotopy and strong deformation retracts. As for the technicity involved, this author likes to think of this material as a vast generalisation of van Oosten’s work on the effective topos [2], so the latter is the leading example here. It turns out that this setting accommodates a model of basic Homotopy Type Theory in the sense of Joyal, since these abstract Hurewicz fibrations can be organised in a type theoretical tribe [1]. The question of univalence [3] is not addressed in this work.[1]André Joyal. Categorical homotopy type theory. https://arxiv.org/abs/1710.10238, 2017.
[2]Jaap Van Oosten. A notion of homotopy for the effective topos. Mathematical Structures in Computer Science, 25(05):1132-1146, 2015.
[3]Vladimir Voevodsky et al. Homotopy type theory: univalent foundations of mathematics. Institute for Advanced Study (Princeton), The Univalent Foundations Program, 2013.

The Coq proof assistant provides an extraction procedure, translating terms in (a variant of) the Calculus of Inductive Constructions to functional programming languages (e.g. OCaml, Haskell or Scheme). This transformation essentially produces untyped realizers from typed terms in dependent type theory, erasing types and proof terms (CIC has a specific sort Prop to categorize propositional types inhabited by proof terms). As part of the MetaCoq[2, 4] project, whose aim is to formalize Coq’s underlying type theory, kernel implementation and related translations, we are formalizing the first phase of this translation, which erases types and proofs. Our erasure function is at the basis of the CertiCoq [1] compiler which translates erased terms to C programs, and could eventually replace Coq’s trusted ML implementation.
Coq’s current erasure was implemented and justified on paper by Letouzey [3], who gives both syntactic and semantic proofs of simulation. The syntactic proof is based on small-step operational semantics, while we employ big-step semantics, simplifying the proof if only closed terms are of interest and naturally supporting separate compilation. In the course of formalization, we have to elaborate all cases in detail (dealing with the peculiar representation of fixpoints for example) and formalize many auxiliary lemmas not surfacing on paper.
Our work can also be seen as a first step towards building verified realizability models for Coq, which could be used to justify the consistency of logical extensions by axioms such as Markov’s principle.[1] Abhishek Anand, Andrew Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A verified compiler for Coq. In CoqPL. Paris, France. http://conf.researchr.org/event/CoqPL-2017/main-certicoq-a-verified-compiler-for-coq
[2] Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. 2018. Towards Certified Meta-Programming with Typed Template-Coq. In ITP 2018 (Lecture Notes in Computer Science), Jeremy Avigad and Assia Mahboubi (Eds.), Vol. 10895. Springer, 20–39. https://doi.org/10.1007/978-3-319-94821-8_2
[3] Pierre Letouzey. 2004. Programmation fonctionnelle certifiée: l’extraction de programmes dans l’assistant Coq. Thèse de Doctorat. Université Paris-Sud. http://www.pps.jussieu.fr/~letouzey/download/these_letouzey.pdf
[4] Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. 2019. The MetaCoq Project. (2019). http://www.irif.fr/~sozeau/research/publications/drafts/The_MetaCoq_Project.pdf Submitted.

We consider the space of probability measures over a given space in the setting of computable analysis in the approach following synthetic topology. We show that over a quasi-Polish space, the space of probability measures inherits both Hausdorffness and compactness from the base space [jww Matthew de Brecht]. With some further machinery, we can then prove that the Haar measure on a compact metric group is computable.

In an impressive series of papers, Krivine showed at the edge of the last decade how classical realizability furnishes a surprising technique to build models for classical theories. In particular, he proved that classical realizability subsumes Cohen’s forcing [3], and even more, gives rise to unexpected models of set theories [4]. Pursuing the algebraic analysis of these models that was first undertaken by Streicher [7, 2], Miquel recently proposed to lay the algebraic foundation of classical realizability and forcing within new structures which he called implicative algebras [5, 6]. These structures are a generalization of Boolean algebras based on an internal law representing the implication. Notably, implicative algebras allow for the adequate interpretation of both programs (i.e. proofs) and their types (i.e. formulas) in the same structure.
The very definition of implicative algebras takes position on a presentation of logic through universal quantification and the implication and, computationally, relies on the call-by-name λ-calculus. In this talk, I propose to investigate the relevance of these choices, by introducing two similar structures. On the one hand, we define disjunctive algebras, relying on internal laws for the negation and the disjunction (reflecting the classical decomposition A → B = ¬A ∨ B) and which we show to be particular cases of implicative algebras. On the other hand, we introduce conjunctive algebras, which rather put the focus on conjunctions and the call-by-value evaluation strategy (reflecting the classical decomposition A → B = ¬(A ∧ ¬B)). We will see that the well-known duality of computation [1] is reflected by simple translations from conjunctive to disjunctive algebras and vice-versa, where the underlying lattices are simply reversed; and that at the level of the induced models, these translations even define tripos isomorphisms.[1] P.-L. Curien and H. Herbelin. The duality of computation. In Proceedings of ICFP 2000, SIGPLAN Notices 35(9), pages 233–243. ACM, 2000. doi:10.1145/351240.351262.
[2] W. Ferrer Santos, J. Frey, M. Guillermo, O. Malherbe, and A. Miquel. Ordered combinatory algebras and realizability. Mathematical Structures in Computer Science, 27(3):428–458, 2017. doi:10.1017/S0960129515000432.
[3] J.-L. Krivine. Realizability algebras: a program to well order r. Logical Methods in Computer Science, 7(3), 2011. doi:10.2168/LMCS-7(3:2)2011.
[4] J.-L. Krivine. Realizability algebras II : new models of ZF + DC. Logical Methods in Computer Science, 8(1):10, Feb. 2012. 28 p. doi:10.2168/LMCS-8(1:10)2012.
[5] A. Miquel. Implicative algebras: a new foundation for realizability and forcing. ArXiv e-prints, 2018. URL: https://arxiv.org/abs/1802.00528, arXiv:1802.00528.
[6] É. Miquey. Formalizing implicative algebras in Coq. In J. Avigad and A. Mahboubi, editors, Interactive Theorem Proving, pages 459–476. Springer International Publishing, 2018. doi:10. 1007/978-3-319-94821-8_27.
[7] T. Streicher. Krivine’s classical realisability from a categorical perspective. Mathematical Structures in Computer Science, 23(6):1234–1256, 2013. doi:10.1017/S0960129512000989.

Randomization is a powerful technique in classical (i.e. discrete) Computer Science: Many difficult problems have turned out to admit simple solutions by algorithms that ‘roll dice’ and are efficient/correct/optimal with high probability. In fact fair coin flips have been shown computationally universal [Wal77]. Our Theorem 3 below formally confirms that fair coins are also universal over continuous data. This extends (and heavily builds on) [SS06, Proposition 13] establishing essentially that suitably and adaptively biased coin flips are universal.
Recall that a measure space is a triple (X, A, μ), where X is a non-empty set, A is a σ-algebra over X, and μ is a measure on (X, A). For measure spaces (X, A, μ) and (Y, B, ν) and a measurable partial mapping F :⊆ X → Y , ν is the pushforward measure of μ w.r.t. F if μ(F^-1[V]) is defined and equal to ν(V) for every V ∈ B. In this case we say F realizes ν on μ and write ν ≼ μ. Realizability is transitive; a realizer F has dom(F ) ∈ A of measure ν(Y ).
Example 1:
a) Consider the real unit interval X = [0, 1] equipped with the σ-algebra A of Borel subsets and the Lebesgues probability measure λ.
b) Consider Cantor space C = {0, 1}^ω equipped with the σ-algebra B of Borel subsets and the canonical (=fair coin flip) probability measure γ: γ( w ◦ C) = 2^−|w| where |w|=n denotes the length of w = (w_0 , . . . , w_n−1 )| ∈ {0, 1}^n
c) The continuous total mapping ρ_b : b ∈ C → Σj≥0 b_j 2^−j−1 ∈ [0, 1] realizes ([0, 1], A, λ) on (C, B, γ): ([0, 1], A, λ) ≼ (C, B, γ).
d) Consider the real line R equipped with (the Borel σ-algebra and) the standard Gaussian/normal probability distribution, realized on λ via the R partial mapping G : t ∈ (0, 1) → Φ^−1(t) ∈ R for the cumulative distribution Φ : s ∈ R → ∫_−∞^s exp(−t^2 /2)/√(2π) dt ∈ [0, 1].
In the sequel we consider topological spaces implicitly equipped with the Borel σ-algebra, and a Borel probability measure. [SS06, Proposition 13] establishes the following:
Fact 2:
To every 2nd countable T 0 space X with Borel probability measure μ there exists a Borel probability measure γ on C such that (X, μ) has a continuous partial realizer over (C, γ).
Theorem 3:
Every Borel probability measure γ on Cantor space C admits a continuous partial realizer over the ‘fair’ measure γ. [Note that this is not a case of Radon-Nikodym.]SS06. Matthias Schröder and Alex Simpson. Representing probability measures using probabilistic processes. Journal of Complexity, 22(6):768–782, 2006.
Wal77. Alastair J. Walker. An efficient method for generating discrete random variables with general distributions. ACM Trans. Math. Softw., 3(3):253–256, September 1977.

Classical realizability is defined by orthogonality and realizability for linear logic is also commonly defined by orthogonality. We study variations on the definition of realizability by orthogonality which capture all of linear, intuitionistic and classical realizability.