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

DOI10.1017/S0960129513000455zbMATH Open1342.03040OpenAlexW2055390302MaRDI QIDQ5740401FDOQ5740401

Authors: 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

Recommendations

• Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)
• Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
• Interactive realizability for classical Peano arithmetic with Skolem axioms
• Constructive forcing, CPS translations and witness extraction in interactive realizability
• Interactive realizers: a new approach to program extraction from nonconstructive proofs

Mathematics Subject Classification ID

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

Cites Work

• Constructivism in mathematics. An introduction. Volume I
• Untersuchungen über das logische Schliessen. II
• Epsilon substitution method for elementary analysis
• Title not available (Why is that?)
• A semantics of evidence for classical arithmetic
• Title not available (Why is that?)
• On the computational content of the axiom of choice
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• Learning based realizability for HA + EM1 and 1-backtracking games: soundness and completeness
• A constructive analysis of learning in Peano arithmetic
• Computer science logic (CSL'11). 25th international workshop, 20th annual conference of the EACSL, Bergen, Norway, September 12--15, 2011.
• Update procedures and the 1-consistency of arithmetic

Cited In (9)

• On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
• Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
• Learning based realizability for HA + EM1 and 1-backtracking games: soundness and completeness
• Interactive realizability for classical Peano arithmetic with Skolem axioms
• A new use of Friedman's translation: interactive realizability
• Constructive forcing, CPS translations and witness extraction in interactive realizability
• A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract)
• Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)
• Interactive realizability and the elimination of Skolem functions in Peano arithmetic

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740401)