Typed realizability for first-order classical analysis

DOI10.2168/LMCS-11(4:22)2015zbMath1351.03006arXiv1512.05313OpenAlexW2280486416MaRDI QIDQ3460427

Valentin Blot

Publication date: 7 January 2016

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1512.05313

zbMATH Keywords

axiom of choiceclassical realizabilitybar recursion\(\lambda\mu\) calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) First-order arithmetic and fragments (03F30) Intuitionistic mathematics (03F55) Axiom of choice and related propositions (03E25) Combinatory logic and lambda calculus (03B40)

This page was built for publication: Typed realizability for first-order classical analysis