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.
| Original language | English |
|---|---|
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 325 |
| Pages (from-to) | 111-126 |
| Number of pages | 16 |
| ISSN | 1571-0661 |
| DOIs | |
| Publication status | Published - 2016 |
| Event | 32nd Conference on the Mathematical Foundations of Programming Semantics - Carnegie Mellon University, Pittsburgh, United States Duration: 23 May 2016 → 26 May 2016 Conference number: 32 |
Conference
| Conference | 32nd Conference on the Mathematical Foundations of Programming Semantics |
|---|---|
| Number | 32 |
| Location | Carnegie Mellon University |
| Country/Territory | United States |
| City | Pittsburgh |
| Period | 23/05/2016 → 26/05/2016 |
Keywords
- Classical realizability
- CPS translation
- ludics
- topos
- tripos