A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus
Category Theory
2019-03-14 v4 Logic
Abstract
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.
Keywords
Cite
@article{arxiv.1407.1547,
title = {A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus},
author = {Thomas Streicher},
journal= {arXiv preprint arXiv:1407.1547},
year = {2019}
}