Thomas Streicher - A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus

lmcs:4129 - Logical Methods in Computer Science, December 7, 2017, Volume 13, Issue 4 - https://doi.org/10.23638/LMCS-13(4:24)2017
A Classical Realizability Model arising from a Stable Model of Untyped Lambda CalculusArticle

Authors: Thomas Streicher

    We study a classical realizability model (in the sense of J.-L. Krivine) arising from a model of untyped lambda calculus in coherence spaces. We show that this model validates countable choice using bar recursion and bar induction.

    https://doi.org/10.23638/LMCS-13(4:24)2017
    Source: arXiv.org:1407.1547
    Volume: Volume 13, Issue 4
    Published on: December 7, 2017
    Accepted on: December 7, 2017
    Submitted on: December 7, 2017
    Keywords: Mathematics - Category Theory,Mathematics - Logic
    Licence: arXiv.org - Non-exclusive license to distribute

    Share and export

    Consultation statistics

    This page has been seen 1603 times.
    This article's PDF has been downloaded 701 times.