Existential witness extraction in classical realizability and via a negative translation
From MaRDI portal
Publication:3003319
DOI10.2168/LMCS-7(2:2)2011zbMath1218.03016MaRDI QIDQ3003319
Publication date: 26 May 2011
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)
Related Items (9)
Realizability for Peano arithmetic with winning conditions in HON games ⋮ Stateful Realizers for Nonstandard Analysis ⋮ Classical realizability and arithmetical formulæ ⋮ A Classical Sequent Calculus with Dependent Types ⋮ Implicative algebras: a new foundation for realizability and forcing ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs ⋮ A Survey of Classical Realizability ⋮ Classical realizability in the CPS target language
This page was built for publication: Existential witness extraction in classical realizability and via a negative translation
