Interactive Learning-Based Realizability for Heyting Arithmetic with EM1
From MaRDI portal
Publication:2786136
DOI10.2168/LMCS-6(3:19)2010zbMath1201.03052arXiv1007.1785MaRDI QIDQ2786136
Stefano Berardi, Federico Aschieri
Publication date: 21 September 2010
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1007.1785
Related Items
On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem, Unnamed Item, A universal algorithm for Krull's theorem, Constructive forcing, CPS translations and witness extraction in Interactive realizability, A constructive analysis of learning in Peano arithmetic, Well Quasi-orders and the Functional Interpretation, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017, Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs, Bar recursion over finite partial functions, GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION