Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1

DOI10.1017/S0960129513000455zbMath1342.03040OpenAlexW2055390302MaRDI QIDQ5740401

Federico Aschieri

Publication date: 26 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129513000455

Mathematics Subject Classification ID

Second- and higher-order arithmetic and fragments (03F35) Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40)

Related Items (2)

On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem ⋮ Constructive forcing, CPS translations and witness extraction in Interactive realizability

Cites Work

• A constructive analysis of learning in Peano arithmetic
• Constructivism in mathematics. An introduction. Volume I
• Untersuchungen über das logische Schliessen. II
• Epsilon substitution method for elementary analysis
• Learning based realizability for HA + EM1 and 1-backtracking games: soundness and completeness
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• On the computational content of the axiom of choice
• A semantics of evidence for classical arithmetic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Interactive Realizability for second-order Heyting arithmetic with EM1 and SK1