文章基本信息

标题：A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus
本地全文：下载
作者：Streicher, Thomas
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2017
卷号：13
期号：4
语种：English
出版社：Technical University of Braunschweig
摘要：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 showthat this model validates countable choice using bar recursion and barinduction.
关键词：Mathematics - Logic;Mathematics - Category Theory