Fundamenta Informaticae - Volume 121, issue 1-4

Authors: Ghilezan, Silvia | Paolini, Luca

Article Type: Other

DOI: 10.3233/FI-2012-769

Citation: Fundamenta Informaticae, vol. 121, no. 1-4, pp. v-vi, 2012

Authors: van Bakel, Steffen

Article Type: Research Article

Abstract: With the eye on defining a type-based semantics, this paper defines intersection and union type assignment for the sequent calculus 𝒳, a substitution-free language that enjoys the Curry-Howard correspondence with respect to the implicative fragment of Gentzen's sequent calculus for classical logic. We investigate the minimal requirements for such a system to be complete (i.e. closed under redex expansion), and show that the non-logical nature of both intersection and union types disturbs the soundness (i.e. closed uder reduction) properties. This implies that this notion of intersection-union type assignment needs to be restricted to satisfy soundness as well, making it unsuitable …to define a semantics. We will look at two (confluent) notions of reduction, called Call-by-Name and Call-by-Value, and prove soundness results for those. Show more

Keywords: Classical Logic, Sequent Calculus, intersection types, union types

DOI: 10.3233/FI-2012-770

Citation: Fundamenta Informaticae, vol. 121, no. 1-4, pp. 1-41, 2012

Authors: Carlier, Sébastien | Wells, J.B.

Article Type: Research Article

Abstract: Expansion is an operation on typings (pairs of type environments and result types) in type systems for the λ-calculus. Expansion was originally introduced for calculating possible typings of a λ-term in systems with intersection types. This paper aims to clarify expansion and make it more accessible to a wider community by isolating the pure notion of expansion on its own, independent of type systems and types, and thereby make it easier for non-specialists to obtain type inference with flexible precision by making use of theory and techniques that were originally developed for intersection types. We redefine expansion as a simple …algebra on terms with variables, substitutions, composition, and miscellaneous constructors such that the algebra satisfies 8 simple axioms and axiom schemas: the 3 standard axioms of a monoid, 4 standard axioms or axiom schemas of substitutions (including one that corresponds to the usual “substitution lemma” that composes substitutions), and 1 very simple axiom schema for expansion itself. Many of the results on the algebra have also been formally checked with the Coq proof assistant. We then take System E, a λ-calculus type system with intersection types and expansion variables, and redefine it using the expansion algebra, thereby demonstrating how a single uniform notion of expansion can operate on both typings and proofs. Because we present a simplified version of System E omitting many features, this may be independently useful for those seeking an easier-to-comprehend version. Show more

DOI: 10.3233/FI-2012-771

Citation: Fundamenta Informaticae, vol. 121, no. 1-4, pp. 43-82, 2012

Authors: Santo, José Espírito | Ivetić, Jelena | Likavec, Silvia

Article Type: Research Article

Abstract: This paper gives a characterisation, via intersection types, of the strongly normalising proof-terms of an intuitionistic sequent calculus (where LJ easily embeds). The soundness of the typing system is reduced to that of a well known typing system with intersection types for the ordinary λ-calculus. The completeness of the typing system is obtained from subject expansion at root position. Next we use our result to analyze the characterisation of strong normalisability for three classes of intuitionistic terms: ordinary λ-terms, ΛJ-terms (λ-terms with generalised application), and λx-terms (λ-terms with explicit substitution). We explain via our system why the type systems in …the natural deduction format for ΛJ and λx known from the literature contain extra, exceptional rules for typing generalised application or substitution; and we show a new characterisation of the β-strongly normalising λ-terms, as a corollary to a PSN-result, relating the λ-calculus and the intuitionistic sequent calculus. Finally, we obtain variants of our characterisation by restricting the set of assignable types to sub-classes of intersection types, notably strict types. In addition, the known characterisation of the β-strongly normalising λ-terms in terms of assignment of strict types follows as an easy corollary of our results. Show more

Keywords: Sequent calculus, strong normalisation, intersection types, intuitionistic logic

DOI: 10.3233/FI-2012-772

Citation: Fundamenta Informaticae, vol. 121, no. 1-4, pp. 83-120, 2012

Authors: Kamareddine, Fairouz | Rahli, Vincent | Wells, J. B.

Article Type: Research Article

Abstract: Reducibility, despite being quite mysterious and inflexible, has been used to prove a number of properties of the λ-calculus and is well known to offer general proofs which can be applied to a number of instantiations. In this paper, we look at two related but different results in λ-calculi with intersection types. 1. We show that one such result (which aims at giving reducibility proofs of Church-Rosser, standardisation and weak normalisation for the untyped λ-calculus) faces serious problems which break the reducibility method. We provide a proposal to partially repair the method. 2. We consider a second result whose purpose …is to use reducibility for typed terms in order to show the Church-Rosser of β-developments for the untyped terms (and hence the Church-Rosser of β-reduction). In this second result, strong normalisation is not needed. We extend the second result to encompass both βI- and βη-reduction rather than simply β-reduction. Show more

Keywords: Lambda-Calculus, Reducibility, Church-Rosser, Developments

DOI: 10.3233/FI-2012-773

Citation: Fundamenta Informaticae, vol. 121, no. 1-4, pp. 121-152, 2012

Authors: Kamareddine, Fairouz | Nour, Karim | Rahli, Vincent | Wells, J. B.

Article Type: Research Article

Abstract: Expansion is a crucial operation for calculating principal typings in intersection type systems. Because the early definitions of expansion were complicated, E-variables were introduced in order to make the calculations easier to mechanise and reason about. Recently, E-variables have been further simplified and generalised to also allow calculating other type operators than just intersection. There has been much work on semantics for type systems with intersection types, but none whatsoever before our work, on type systems with E-variables. In this paper we expose the challenges of building a semantics for E-variables and we provide a novel solution. Because it is …unclear how to devise a space of meanings for E-variables, we develop instead a space of meanings for types that is hierarchical. First, we index each type with a natural number and show that although this intuitively captures the use of E-variables, it is difficult to index the universal type ω with this hierarchy and it is not possible to obtain completeness of the semantics if more than one E-variable is used. We then move to a more complex semantics where each type is associated with a list of natural numbers and establish that both ω and an arbitrary number of E-variables can be represented without losing any of the desirable properties of a realisability semantics. Show more

Keywords: Realisability semantics, expansion variables, intersection types, completeness

DOI: 10.3233/FI-2012-774

Citation: Fundamenta Informaticae, vol. 121, no. 1-4, pp. 153-184, 2012

Authors: Koletsos, George

Article Type: Research Article

Abstract: We use the system of intersection types and the type assignment method to prove termination properties in λ-calculus. In the first part we deal with conservation properties. We give a type assignment proof of the classical conservation theorem for λI calculus and then we extend this method to the notion of the reduction βI and βS of de Groote [9]. We also give a direct type assignment proof of the extended conservation property according to which if a term is βI , βS -normalizable then it is β-strongly normalizable. We further extend the conservation theorem by introducing the …notion of β* -normal form. In the second part we prove that if Ω is not a substring of a λ-term M then M can be typed in the Krivine's system D of intersection types. In that way we obtain a type assignment proof of the Sørensen's Ω-theorem. Show more

DOI: 10.3233/FI-2012-775

Citation: Fundamenta Informaticae, vol. 121, no. 1-4, pp. 185-202, 2012

Authors: Laurent, Olivier

Article Type: Research Article

Abstract: We give a purely syntactic proof (from scratch) of the subject equality property of the BCD intersection type system through a reformulation of the subtyping relation having a “cut-elimination” property.

DOI: 10.3233/FI-2012-776

Citation: Fundamenta Informaticae, vol. 121, no. 1-4, pp. 203-226, 2012

Authors: Piccolo, Mauro

Article Type: Research Article

Abstract: In this work we present an extension of the linear typing discipline for π-calculus, introduced by Yoshida, Honda and Berger, with Intersection and Union Types. We show that we are able to define a typing system for the π-calculus, which guarantees that every well-typed term is strongly normalizing. This typing system is an extension of that presented in [30] since it is able to type more terms than that presented there.

DOI: 10.3233/FI-2012-777

Citation: Fundamenta Informaticae, vol. 121, no. 1-4, pp. 227-252, 2012

Authors: Pimentel, Elaine | Ronchi Della Rocca, Simona | Roversi, Luca

Article Type: Research Article

Abstract: In this work we present a proof-theoretical justification for the intersection type assignment system (IT) by means of the logical system Intersection Synchronous Logic (ISL). ISL builds classes of equivalent deductions of the implicative and conjunctive fragment of the intuitionistic logic (NJ). ISL results from decomposing intuitionistic conjunction into two connectives: a synchronous conjunction, that can be used only among equivalent deductions of NJ, and an asynchronous one, that can be applied among any sets of deductions of NJ. A term decoration of ISL exists so that it matches both: the IT assignment system, when only the synchronous conjunction is …used, and the simple types assignment with pairs and projections, when the asynchronous conjunction is used. Moreover, the proof of strong normalization property for ISL is a simple consequence of the same property in NJ and hence strong normalization for IT comes for free. Show more

Keywords: Intersection types, λ-calculus, type assignment systems, structural proof-theory

DOI: 10.3233/FI-2012-778

Citation: Fundamenta Informaticae, vol. 121, no. 1-4, pp. 253-274, 2012