Classical realizability in the CPS target language

Publikation: Bidrag til tidsskrift › Konferenceartikel › Forskning › fagfællebedømt

Standard

Classical realizability in the CPS target language. / Frey, Jonas.

I: Electronic Notes in Theoretical Computer Science, Bind 325, 2016, s. 111-126.

Publikation: Bidrag til tidsskrift › Konferenceartikel › Forskning › fagfællebedømt

Harvard

Frey, J 2016, 'Classical realizability in the CPS target language', Electronic Notes in Theoretical Computer Science, bind 325, s. 111-126. https://doi.org/10.1016/j.entcs.2016.09.034

APA

Frey, J. (2016). Classical realizability in the CPS target language. Electronic Notes in Theoretical Computer Science, 325, 111-126. https://doi.org/10.1016/j.entcs.2016.09.034

Vancouver

Frey J. Classical realizability in the CPS target language. Electronic Notes in Theoretical Computer Science. 2016;325:111-126. https://doi.org/10.1016/j.entcs.2016.09.034

Author

Frey, Jonas. / Classical realizability in the CPS target language. I: Electronic Notes in Theoretical Computer Science. 2016 ; Bind 325. s. 111-126.

Bibtex

@inproceedings{65185674b0ca4398b7ea41a12e4baaa1,
title = "Classical realizability in the CPS target language",
abstract = "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.",
keywords = "Classical realizability, CPS translation, ludics, topos, tripos",
author = "Jonas Frey",
year = "2016",
doi = "10.1016/j.entcs.2016.09.034",
language = "English",
volume = "325",
pages = "111--126",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
note = "null ; Conference date: 23-05-2016 Through 26-05-2016",

}

RIS

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

VL - 325

SP - 111

EP - 126

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

Y2 - 23 May 2016 through 26 May 2016

ER -

ID: 172100185