Classical realizability in the CPS target language

TY - GEN

T1 - Classical realizability in the CPS target language

AU - Frey, Jonas

N1 - Conference code: 32

PY - 2016

Y1 - 2016

N2 - Motivated by considerations about Krivine's classical realizability, we introduce a term calculus for an intuitionistic logic with record types, which we call the CPS target language. We give a reformulation of the constructions of classical realizability in this language, using the categorical techniques of realizability triposes and toposes. We argue that the presentation of classical realizability in the CPS target language simplifies calculations in realizability toposes, in particular it admits a nice presentation of conjunction as intersection type which is inspired by Girard's ludics.

AB - Motivated by considerations about Krivine's classical realizability, we introduce a term calculus for an intuitionistic logic with record types, which we call the CPS target language. We give a reformulation of the constructions of classical realizability in this language, using the categorical techniques of realizability triposes and toposes. We argue that the presentation of classical realizability in the CPS target language simplifies calculations in realizability toposes, in particular it admits a nice presentation of conjunction as intersection type which is inspired by Girard's ludics.

KW - Classical realizability

KW - CPS translation

KW - ludics

KW - topos

KW - tripos

UR - http://www.scopus.com/inward/record.url?scp=84992420224&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2016.09.034

DO - 10.1016/j.entcs.2016.09.034

M3 - Conference article

AN - SCOPUS:84992420224

SN - 1571-0661

VL - 325

SP - 111

EP - 126

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

T2 - 32nd Conference on the Mathematical Foundations of Programming Semantics

Y2 - 23 May 2016 through 26 May 2016

ER -