Fundamenta Informaticae - Volume 84, issue 2

Article Type: Other

Citation: Fundamenta Informaticae, vol. 84, no. 2, pp. i-iii, 2008

Authors: Asher, Nicholas

Article Type: Research Article

Abstract: 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.

Keywords: complex types,, lambda calculus,, categorial interpretation,, copredication,, coercion,, dot(•)types

Citation: Fundamenta Informaticae, vol. 84, no. 2, pp. 151-183, 2008

Authors: Biasi, Corrado | Aschieri, Federico

Article Type: Research Article

Abstract: 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. Show more

Keywords: subtractive logic, bi-intuitionistic logic, intuitionistic logic for pragmatics, lambda calculus, strong normalization

Citation: Fundamenta Informaticae, vol. 84, no. 2, pp. 185-205, 2008

Authors: Oliva, Paulo | Streicher, Thomas

Article Type: Research Article

Abstract: 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. Show more

Citation: Fundamenta Informaticae, vol. 84, no. 2, pp. 207-220, 2008

Authors: Power, John | Tanaka, Miki

Article Type: Research Article

Abstract: 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. Show more

Keywords: pseudo-monad, pseudo-distributive law, binding, substitutionmonoidal structure, binding signature

Citation: Fundamenta Informaticae, vol. 84, no. 2, pp. 221-240, 2008

Authors: Raffalli, Christophe | Ruyer, Frédéric

Article Type: Research Article

Abstract: 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.

Citation: Fundamenta Informaticae, vol. 84, no. 2, pp. 241-258, 2008

Authors: White, Graham

Article Type: Research Article

Citation: Fundamenta Informaticae, vol. 84, no. 2, pp. 259-289, 2008