Classical realizability in the CPS target language

Research output: Contribution to journalConference articlepeer-review

Documents

  • Jonas Frey

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.

Original languageEnglish
JournalElectronic Notes in Theoretical Computer Science
Volume325
Pages (from-to)111-126
Number of pages16
ISSN1571-0661
DOIs
Publication statusPublished - 2016
Event32nd Conference on the Mathematical Foundations of Programming Semantics - Carnegie Mellon University, Pittsburgh, United States
Duration: 23 May 201626 May 2016
Conference number: 32

Conference

Conference32nd Conference on the Mathematical Foundations of Programming Semantics
Number32
LocationCarnegie Mellon University
CountryUnited States
CityPittsburgh
Period23/05/201626/05/2016

    Research areas

  • Classical realizability, CPS translation, ludics, topos, tripos

Number of downloads are based on statistics from Google Scholar and www.ku.dk


No data available

ID: 172100185