Classical realizability and side-effects

Étienne Miquey 1, 2
2 PI.R2 - Design, study and implementation of languages for proofs and programs
Inria de Paris, CNRS - Centre National de la Recherche Scientifique, UPD7 - Université Paris Diderot - Paris 7, PPS - Preuves, Programmes et Systèmes
Abstract : This thesis focused on the computational content of classical proofs, and specifically on proofs with side-effects and Krivine classical realizability. The manuscript is divided in three parts, the first of which consists of a detailed introduction to the concepts used in the sequel. The second part deals with the computational content of the axiom of dependent choice in classical logic. This works is in the continuity of dPAω system of Hugo Herbelin, which allows to adapt the constructive proof of the axiom of choice in Martin-Löf's type theory in order to turn it into a constructive proof of the axiom of dependent choice in a setting compatible with classical logic. The principal goal of this part is to prove the property of normalization for dPAω, on which relies the consistency of the system. Such a proof is hard to obtain, due to the simultaneous presence of dependent types (for the constructive part of the choice), of control operators (for classical logic), of co-inductive objects (in order to "encode" functions of type N → A as streams (a₀,a₁,...)) and of lazy evaluation with sharing (for this co-inductive objects). This difficulties are first studied separately. In particular, we show the normalization of classical call-by-need (presented as an extension of the λµ̃µ-calculus with shared environments) by means of realizability techniques. Next, we develop a classical sequent calculus with dependent types, defined again as an adaptation of the λµ̃µ-calcul whose soundness is proved thanks to a CPS-translation which takes the dependencies into account. Last, a sequent-calculus variant of dPAω is introduced, combining the two previous systems. Its normalization is finally proved using realizability techniques. The last part, more oriented towards semantics, studies the duality between the call-by-name and call-by-value evaluation strategies in a purely algebraic setting, inspired from several works around classical realizability (and in particular Krivine realizability algebras). This work relies on the notion of implicative algebras developed by Alexandre Miquel, a very simple algebraic structure generalizing at the same time complete Boolean algebras and Krivine realizability algebras, in such a way that it allows to express in a same setting the theory of forcing (in the sense of Cohen) and the theory of classical realizability (in the sense of Krivine). The main default of these structures is that they are deeply oriented towards the λ-calculus, and that they only allows to faithfully interpret languages in call-by-name. To remediate the situation, we introduce two variants of implicative algebras: disjunctive algebras, centered on the "par" connective of linear logic (but in a non-linear framework) and naturally adapted to languages in call-by-name; and conjunctives algebras, centered on the "tensor" connective of linear logic and adapted to languages in call-by-value. Amongst other things, we show that disjunctive algebras are particular cases of implicative algebras and that conjunctive algebras can be obtained from disjunctive algebras (by reversing the underlying order). Moreover, we show how to interpret in these framework the fragments of Guillaume Munch-Maccagnoni's system L for call-by-value (within conjunctive algebras) and for call-by-name (within disjunctive algebras).
Document type :
Theses
Complete list of metadatas

Cited literature [153 references]  Display  Hide  Download

https://hal.inria.fr/tel-01653733
Contributor : Étienne Miquey <>
Submitted on : Sunday, December 31, 2017 - 12:55:30 PM
Last modification on : Friday, February 22, 2019 - 11:16:45 AM

File

these.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-01653733, version 2

Collections

Citation

Étienne Miquey. Classical realizability and side-effects. Logic in Computer Science [cs.LO]. Université Sorbonne Paris Cité - Université Paris Diderot (Paris 7); Universidad de la República - Montevideo, Uruguay, 2017. English. ⟨tel-01653733v2⟩

Share

Metrics

Record views

209

Files downloads

232