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.

@article{Streicher17,
  title = {A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus},
  author = {Thomas Streicher},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 13, Issue 4},
  year = {2017},
  doi = {10.23638/lmcs-13(4:24)2017}
}