This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
Modified bar recursion has been used to give a realizability interpretation of the classical axioms of countable and dependent choice. In this paper we survey the main results con...
This article investigates Krivine's realizability interpretation of classical second-order arithmetic and its recent extension handling countable choice. We will start by pre...
RZ is a tool which translates axiomatizations of mathematical structures to program specifications using the realizability interpretation of logic. This helps programmers correctl...
Abstract. We propose a new operational model for shared variable concurrency, in the context of a concurrent, higher-order imperative language `a la ML. In our model the scheduling...