Relating Classical Realizability and Negative Translation for Existential Witness Extraction

DOI10.1007/978-3-642-02273-9_15zbMath1218.03015OpenAlexW1856816820MaRDI QIDQ3637195

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

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

Uses Software

• Coq

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• Dependent choice, `quote' and the clock
• Classical Program Extraction in the Calculus of Constructions
• Typed lambda-calculus in classical Zermelo-Fraenkel set theory
• Unnamed Item
• Unnamed Item

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