Streicher, Thomas - A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus

lmcs:4129 - Logical Methods in Computer Science, December 7, 2017, Volume 13, Issue 4
A Classical Realizability Model arising from a Stable Model of Untyped Lambda Calculus

Authors: Streicher, Thomas

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.


Source : oai:arXiv.org:1407.1547
DOI : DOI:10.23638/LMCS-13(4:24)2017
Volume: Volume 13, Issue 4
Published on: December 7, 2017
Submitted on: December 7, 2017
Keywords: Mathematics - Category Theory,Mathematics - Logic


Share

Browsing statistics

This page has been seen 25 times.
This article's PDF has been downloaded 16 times.