Classical realizability in the CPS target language

Jonas Frey

Publikation: Bidrag til tidsskriftKonferenceartikelForskningpeer review

1 Citationer (Scopus)
192 Downloads (Pure)

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.

OriginalsprogEngelsk
TidsskriftElectronic Notes in Theoretical Computer Science
Vol/bind325
Sider (fra-til)111-126
Antal sider16
ISSN1571-0661
DOI
StatusUdgivet - 2016
Begivenhed32nd Conference on the Mathematical Foundations of Programming Semantics - Carnegie Mellon University, Pittsburgh, USA
Varighed: 23 maj 201626 maj 2016
Konferencens nummer: 32

Konference

Konference32nd Conference on the Mathematical Foundations of Programming Semantics
Nummer32
LokationCarnegie Mellon University
Land/OmrådeUSA
ByPittsburgh
Periode23/05/201626/05/2016

Citationsformater