Classical realizability in the CPS target language

DOI10.1016/J.ENTCS.2016.09.034zbMath1394.68060OpenAlexW2527684024WikidataQ113317638 ScholiaQ113317638MaRDI QIDQ1744381

Jonas Frey

Publication date: 23 April 2018

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

zbMATH Keywords

toposclassical realizabilityludicsCPS translationtripos

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Computational ludics
• Resource modalities in tensor logic
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Dual-intuitionistic logic
• On full abstraction for PCF: I, II and III
• A call-by-name lambda-calculus machine
• On the unity of duality
• Control categories and duality: on the categorical semantics of the lambda-mu calculus
• Locus Solum: From the rules of logic to the logic of rules
• The duality of computation
• Existential witness extraction in classical realizability and via a negative translation
• The Duality of Computation under Focus
• Tripos theory
• A new constructive logic: classic logic
• Classical logic, continuation semantics and abstract machines
• A semantics of evidence for classical arithmetic
• Realizability Toposes from Specifications

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