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

Autor:	Thomas Streicher
Jazyk:	angličtina
Rok vydání:	2017
Předmět:	mathematics - category theory mathematics - logic Logic BC1-199 Electronic computers. Computer science QA75.5-76.95
Zdroj:	Logical Methods in Computer Science, Vol Volume 13, Issue 4 (2017)
Druh dokumentu:	article
ISSN:	1860-5974
DOI:	10.23638/LMCS-13(4:24)2017
Popis:	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.
Databáze:	Directory of Open Access Journals
Externí odkaz:	https://doaj.org/article/f1e9599fc65f4151a5bfb81f06844519 Zobrazit plný text záznamu View record in DOAJ