Relating Classical Realizability and Negative Translation for Existential Witness Extraction

DOI10.1007/978-3-642-02273-9_15MaRDI QIDQ3637195zbMATH OpenOpenAlexFDO

Authors Alexandre Miquel

Publication date 7 July 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02273-9_15

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Second- and higher-order arithmetic and fragments (03F35) Intuitionistic mathematics (03F55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Existential witness extraction in classical realizability and via a negative translation
• scientific article; zbMATH DE number 895269
• Constructive forcing, CPS translations and witness extraction in interactive realizability
• A Survey of Classical Realizability
• scientific article; zbMATH DE number 65537

Cites work

• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• Classical Program Extraction in the Calculus of Constructions
• Dependent choice, `quote' and the clock
• scientific article; zbMATH DE number 5360217 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Typed lambda-calculus in classical Zermelo-Fraenkel set theory

Cited in

(8)

• A constructive valuation semantics for classical logic
• A realizability interpretation for classical analysis
• Extracting Herbrand trees in classical realizability using forcing
• Existential witness extraction in classical realizability and via a negative translation
• A translation characterizing the constructive content of classical theories
• scientific article; zbMATH DE number 895269 (Why is no real title available?)
• scientific article; zbMATH DE number 1420833 (Why is no real title available?)
• Constructive forcing, CPS translations and witness extraction in interactive realizability

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Relating Classical Realizability and Negative Translation for Existential Witness Extraction

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