Realizability Toposes from Specifications

TL;DR

This paper develops a framework linking realizability models to process specifications with I/O effects, enabling the construction of toposes from computational and behavioral properties.

Contribution

It introduces a method to associate realizability models to I/O specifications using poles and proof-like terms, extending realizability to computable functions and toposes.

Findings

Models give rise to triposes and toposes

Framework handles I/O effects in realizability

Associates realizability models with computable functions

Abstract

We investigate a framework of Krivine realizability with I/O effects, and present a method of associating realizability models to specifications on the I/O behavior of processes, by using adequate interpretations of the central concepts of `pole' and `proof-like term'. This method does in particular allow to associate realizability models to computable functions. Following recent work of Streicher and others we show how these models give rise to triposes and toposes.