Interactive realizers: a new approach to program extraction from nonconstructive proofs

DOI10.1145/2159531.2159533MaRDI QIDQ2946659zbMATH OpenOpenAlexFDO

Authors Stefano Berardi, Ugo de'Liguoro

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2159531.2159533

zbMATH Keywords

constructive interpretations of classical logiclearning in the limitrealizability

Mathematics Subject Classification ID

Logic in computer science (03B70) First-order arithmetic and fragments (03F30) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computational learning theory (68Q32)

Recommendations

• A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract)
• Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
• Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)
• scientific article; zbMATH DE number 895269
• Interactive realizability for classical Peano arithmetic with Skolem axioms

Cited in

(13)

• Uniform Heyting arithmetic
• On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
• scientific article; zbMATH DE number 1629956 (Why is no real title available?)
• Interactive learning-based realizability for Heyting arithmetic with \(\mathrm{EM}_1\)
• A Calculus of Realizers for EM 1 Arithmetic (Extended Abstract)
• Interactive Learning-Based Realizability Interpretation for Heyting Arithmetic with EM 1
• Interactive realizability for classical Peano arithmetic with Skolem axioms
• scientific article; zbMATH DE number 7393562 (Why is no real title available?)
• Interpreting a classical geometric proof with interactive realizability
• Interactive learning based realizability and 1-backtracking games
• Constructive forcing, CPS translations and witness extraction in interactive realizability
• Interactive realizability for second-order Heyting arithmetic with EM1 and SK1
• Extraction of redundancy-free programs from constructive natural deduction proofs

This page was built for publication: Interactive realizers: a new approach to program extraction from nonconstructive proofs

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