Classical realizability in the CPS target language

DOI10.1016/J.ENTCS.2016.09.034MaRDI QIDQ1744381zbMATH OpenOpenAlexWikidataFDO

Authors Jonas Frey

Publication date 23 April 2018

Full work available at URL https://doi.org/10.1016/j.entcs.2016.09.034

zbMATH Keywords

classical realizabilityCPS translationludicstopostripos

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40) Categorical logic, topoi (03G30) Functional programming and lambda calculus (68N18)

Recommendations

• Constructive classical logic as CPS-calculus
• A Survey of Classical Realizability
• Focalisation and Classical Realisability
• Krivine's classical realisability from a categorical perspective
• scientific article; zbMATH DE number 5851813

Cites work

• A call-by-name lambda-calculus machine
• A new constructive logic: classic logic
• A semantics of evidence for classical arithmetic
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Classical logic, continuation semantics and abstract machines
• Computational ludics
• Control categories and duality: On the categorical semantics of the lambda-mu calculus
• Dual-intuitionistic logic
• Existential witness extraction in classical realizability and via a negative translation
• scientific article; zbMATH DE number 5851813 (Why is no real title available?)
• scientific article; zbMATH DE number 3970744 (Why is no real title available?)
• scientific article; zbMATH DE number 3614784 (Why is no real title available?)
• scientific article; zbMATH DE number 1231584 (Why is no real title available?)
• Locus solum: From the rules of logic to the logic of rules.
• On full abstraction for PCF: I, II and III
• On the unity of duality
• Realizability toposes from specifications
• Resource modalities in tensor logic
• The duality of computation
• The duality of computation under focus
• The stack calculus
• Tripos theory

Cited in

(1)

• Classical realizability as a classifier for nondeterminism

This page was built for publication: Classical realizability in the CPS target language

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