A Survey of Classical Realizability

DOI10.1007/978-3-642-21691-6_1MaRDI QIDQ3007652zbMATH OpenOpenAlexFDO

Authors Alexandre Miquel

Publication date 17 June 2011

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-21691-6_1

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Recommendations

• REALIZING REALIZABILITY RESULTS WITH CLASSICAL CONSTRUCTIONS
• Classical and relative realizability
• A realizability interpretation for classical analysis
• Publication:4944901
• scientific article; zbMATH DE number 5851813
• Classical realizability as a classifier for nondeterminism
• Classical realizability and arithmetical formulæ
• Quantitative classical realizability
• Verificationism and Classical Realizability

Cites work

• scientific article; zbMATH DE number 5360217 (Why is no real title available?)
• Classical Program Extraction in the Calculus of Constructions
• Dependent choice, `quote' and the clock
• Existential witness extraction in classical realizability and via a negative translation
• On the interpretation of intuitionistic number theory
• THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
• Typed lambda-calculus in classical Zermelo-Fraenkel set theory

Cited in

(18)

• scientific article; zbMATH DE number 845621 (Why is no real title available?)
• Verificationism and Classical Realizability
• A first-order completeness result about characteristic Boolean algebras in classical realizability
• Classical and relative realizability
• Quantitative classical realizability
• Realizability: a historical essay
• Classical realizability and arithmetical formulæ
• Krivine's classical realisability from a categorical perspective
• A semantics of realisability for the classical propositional natural deduction
• Relating Classical Realizability and Negative Translation for Existential Witness Extraction
• Computational interpretations of classical reasoning: from the epsilon calculus to stateful programs
• Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model
• Zeta functions and the (linear) logic of Markov processes
• A correspondence between maximal abelian sub-algebras and linear logic fragments
• Classical realizability in the CPS target language
• Classical realizability as a classifier for nondeterminism
• A quick overview on the quantum control approach to the lambda calculus
• Specifying Peirce's law in classical realizability

This page was built for publication: A Survey of Classical Realizability

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