Fundamenta Informaticae

This paper investigates several models of the complex type • which is needed to analyze copredication. Previous accounts are shown to be inadequate and a new account both of • and copredication is proposed.

We propose a term assignment (let calculus) for Intuitionistic Logic for Pragmatics ILP _{AC} , a polarized sequent calculus which includes ordinary positive intuitionistic logic LJ ^{⊃∩} , its dual LJ ^{∖γ} and dual negations ( ) ^{⊥} which allow a formula to "communicate" with its dual fragment. We prove the strong normalization property for the term assignment which follows by soundly translating the let calculus into simply typed γ calculus with pairings and projections. A new and simple proof of strong normalization for the latter is also provided.

This article investigates Krivine's realizability interpretation of classical second-order arithmetic and its recent extension handling countable choice. We will start by presenting a twostep interpretation which first eliminates classical logic via a negative translation and then applies standard realizability interpretation. We then argue that a slight variant of Krivine's interpretation corresponds to this two-step interpretation. This variant can be viewed as the continuation passing style variant of Krivine's original interpretation, and as such uses standard λ-terms and avoids the use of new continuation constants in the interpretation of classical logic.

We generalise Fiore et al's account of variable binding for untyped cartesian contexts to give an account of binding for either variables or names that may be typed. We do this in an enriched setting, allowing the incorporation of recursion into the analysis. Extending earlier work by us, we axiomatise the notion of context by defining and using the notion of an enriched pseudo-monad S on V-Cat, with leading examples of V given by Set and ωCpo, the latter yielding an account of recursion. Fiore et al implicitly used the pseudo-monad T _{fp} on Cat for small categories with finite products. Given a set A of types, our extension to typed binders and enrichment involves generalising from Fiore et al's use of [F, Set] to [(SA) ^{op} , V ^{A} ]. We define a substitution monoidal structure on [(SA) ^{op} , V ^{A} ], allowing us to give a definition of binding signature at this level of generality, and extend initial algebra semantics to the typed, enriched axiomatic setting. This generalises and axiomatises previouswork by Fiore et al and later authors in particular cases. In particular, it includes the Logic of Bunched Implications and variants, infinitary examples, and structures not previously considered such as those generated by finite limits.

This paper is an introduction to recent works in realizability, mainly Krivine's work to realize the dependent choice axiom. We also show how to improve programs extracted from classical proofs by distinguishing formulas with and without algorithmic contents.