Name
Abstract | ||
|---|---|---|
We propose the new concept of Krivine ordered combinatory algebra ((K)OCA) as foundation for the categorical study of Krivine's classical realizability, as initiated by Streicher (2013). We show that (K)OCA's are equivalent to Streicher's abstract Krivine structures for the purpose of modeling higher-order logic, in the precise sense that they give rise to the same class of triposes. The difference between the two representations is that the elements of a (K)OCA play both the role of truth values and realizers, whereas truth values are sets of realizers in AKSs. To conclude, we give a direct presentation of the realizability interpretation of a higher order language in a (K)OCA, which showcases the dual role that is played by the elements of the (K)OCA. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1017/S0960129515000432 | MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE |
Field | DocType | Volume |
Discrete mathematics,Categorical variable,Pure mathematics,Preorder,Equivalence (measure theory),Mathematics,Realizability | Journal | 27 |
Issue | ISSN | Citations |
3 | 0960-1295 | 0 |
PageRank | References | Authors |
0.34 | 0 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| walter ferrer santos | 1 | 0 | 1.01 |
| jonas frey | 2 | 0 | 0.34 |
| mauricio guillermo | 3 | 0 | 1.01 |
| octavio malherbe | 4 | 0 | 0.34 |
| alexandre miquel | 5 | 0 | 0.34 |