Classical realizability in the CPS target language
Publikation: Bidrag til tidsskrift › Konferenceartikel › Forskning › fagfællebedømt
Dokumenter
- Frey_2016_Classical_realizability
Forlagets udgivne version, 271 KB, PDF-dokument
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.
Originalsprog | Engelsk |
---|---|
Tidsskrift | Electronic Notes in Theoretical Computer Science |
Vol/bind | 325 |
Sider (fra-til) | 111-126 |
Antal sider | 16 |
ISSN | 1571-0661 |
DOI | |
Status | Udgivet - 2016 |
Begivenhed | 32nd Conference on the Mathematical Foundations of Programming Semantics - Carnegie Mellon University, Pittsburgh, USA Varighed: 23 maj 2016 → 26 maj 2016 Konferencens nummer: 32 |
Konference
Konference | 32nd Conference on the Mathematical Foundations of Programming Semantics |
---|---|
Nummer | 32 |
Lokation | Carnegie Mellon University |
Land | USA |
By | Pittsburgh |
Periode | 23/05/2016 → 26/05/2016 |
Antal downloads er baseret på statistik fra Google Scholar og www.ku.dk
Ingen data tilgængelig
ID: 172100185