A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus
classification
🧮 math.CT
math.LO
keywords
modelarisingcalculusclassicallambdarealizabilityuntypedchoice
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.