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

DOI10.1017/S0960129513000455MaRDI QIDQ5740401zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cites work

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

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)