English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

In an impressive series of papers, Krivine showed at the edge of the lastdecade how classical realizability provides a surprising technique to buildmodels for classical theories. In particular, he proved that classicalrealizability subsumes Cohen's forcing, and even more, gives rise to unexpectedmodels of set theories. Pursuing the algebraic analysis of these models thatwas first undertaken by Streicher, Miquel recently proposed to lay thealgebraic foundation of classical realizability and forcing within newstructures which he called implicative algebras. These structures are ageneralization of Boolean algebras based on an internal law representing theimplication. Notably, implicative algebras allow for the adequateinterpretation of both programs (i.e. proofs) and their types (i.e. formulas)in the same structure. The very definition of implicative algebras takesposition on a presentation of logic through universal quantification and theimplication and, computationally, relies on the call-by-name$\lambda$-calculus. In this paper, we investigate the relevance of this choice,by introducing two similar structures. On the one hand, we define disjunctivealgebras, which rely on internal laws for the negation and the disjunction andwhich we show to be particular cases of implicative algebras. On the otherhand, we introduce conjunctive algebras, which rather put the focus onconjunctions and on the call-by-value evaluation strategy. We finally show howdisjunctive and conjunctive algebras algebraically reflect the well-knownduality of computation between call-by-name and call-by-value.

Revisiting the duality of computation: an algebraic analysis of classical realizability models