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

TL;DR

This paper constructs a classical realizability model based on untyped lambda calculus in coherence spaces, demonstrating that it validates countable choice through bar recursion and bar induction.

Contribution

It introduces a new realizability model derived from untyped lambda calculus in coherence spaces that validates countable choice, expanding the understanding of realizability models.

Findings

Model validates countable choice using bar recursion.

Model validates countable choice using bar induction.

Connects classical realizability with untyped lambda calculus in coherence spaces.

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.