Search

We consider a notion of approximation for terms of de Groote–Saurin Λμ-calculus. Then, we introduce an intersection type assignment system for that calculus which is invariant under subject conversion. The type assignment system also induces a filter model, which is an extensional Λμ-model in the sense of Nakazawa and Katsumata. We then establish the approximation theorem, stating that a type can be assigned to a term in the system if and only if it can be assigned to same of its approximations.

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.

This paper gives a new proof for the approximation theorem and the characterisation of normalisability using intersection types for a system with ‘w and a ≤-relation that is contra-variant over arrow types. The technique applied is to define reduction on derivations and to show a strong normalisation result for this reduction. From this result, the characterisation of strong normalisation and the approximation result will follow easily; the latter, in its turn, will lead to the characterisation of (head) normalisability.

Intersection types are well known to type theorists mainly for two reasons. Firstly, they type all and only the strongly normalizable lambda terms. Secondly, the intersection type operator is a meta-level operator, that is, there is no direct logical counterpart in the Curry–Howard isomorphism sense. In particular, its meta-level nature implies that it does not correspond to the intuitionistic conjunction.The intersection type system is naturally a type inference system (system à la Curry), but the meta-level nature of the intersection operator does not allow to easily design an equivalent typed system (system à la Church). There are many proposals in the literature to design such systems, but none of them gives an entirely satisfactory answer to the problem. In this paper, we will review the main results in the literature both on the logical interpretation of intersection types and on proposed typed lambda calculi.The core of this paper is a new proposal for a true intersection typed lambda calculus, without any meta-level notion. Namely, any typable term (in the intersection type inference) has a corresponding typed term (which is the same as the untyped term by erasing the type decorations and the typed term constructors) with the same type, and vice versa.The main idea is to introduce a relevant parallel term constructor which corresponds to the intersection type constructor, in such a way that terms in parallel share the same resources, that is, the same context of free typed variables. Three rules allow us to generate all typed terms. The first two rules, Application and Lambda-abstraction, are performed on all the components of a parallel term in a synchronized way. Finally, via the third rule of Local Renaming, once a free typed variable is bounded by lambda-abstraction, each of the terms in parallel can do its local renaming, with type refinement, of that particular resource.

In this paper we introduce a new filter model, which is of a kind that has escaped investigation up to now: it is induced by an intersection type theory generated in a non-standard way, by a preorder which puts into relation an atom with an arrow type, without equating them. We study the domain-theoretic implications of this choice, that are not trivial: in order to describe this filter model a new category is introduced and a special purpose functor defined. The filter model is then characterized as the initial algebra of the functor.

We present a system of refinement types for LF in the style of recent formulations where only canonical forms are well-typed. Both the usual LF rules and the rules for type refinements are bidirectional, leading to a straightforward proof of decidability of type-checking even in the presence of intersection types. Because we insist on canonical forms, structural rules for subtyping can now be derived rather than being assumed as primitive. We illustrate the expressive power of our system with several examples in the domain of logics and programming languages.

Invariance of interpretation by β-conversion is one of the minimal requirements for any standard model for the λ-calculus. With the intersection-type systems being a general framework for the study of semantic domains for the λ-calculus, the present paper provides a (syntactic) characterisation of the above mentioned requirement in terms of characterisation results for intersection-type assignment systems.Instead of considering conversion as a whole, reduction and expansion will be considered separately. Not only for usual computational rules like β, η, but also for a number of relevant restrictions of those. Characterisations will be also provided for (intersection) filter structures that are indeed λ-models.

We introduce channel sequence types to study finitary polymorphism in the context of mobile processes modelled in the π-calculus. We associate to each channel a set of exchange types, and we require that output processes send values of one of those types, and input processes accept values of any type in the set. Our type assignment system enjoys subject reduction and guarantees the absence of communication errors. We give several examples of polymorphism, and we encode the λ-calculus with the strict intersection type discipline.

International audience; In this paper, we presents a comfortable fully typed lambda calculus based on the well-known intersection type system discipline where proof are not only feasible but easy; the present system is the counterpart à la Church of the type assignment system as invented by Coppo and Dezani.

Modus ponens provides the central theme. There are laws, of the form A → C . A logic (or other theory) L collects such laws. Any datum A (or theory T incorporating such data) provides input to the laws of L . The central ternary relation R relates theories L , T and U , where U consists of all of the outputs C got by applying modus ponens to major premises from L and minor premises from T . Underlying this relation is a modus ponens product (or fusion) operation ∘ on theories (or other collections of formulas) L and T , whence RLTU iff L ∘ T ⊆ U . These ideas have been expressed, especially with Routley, as (Kripke style) worlds semantics for relevant and other substructural logics. Worlds are best demythologized as theories, subject to truth-functional and other constraints. The chief constraint is that theories are taken as closed under logical entailment, which clearly begs the question if we are using the semantics to determine which theory L is Logic itself. Instead we draw the modal logicians’ conclusion—there are many substructural logics, each with its appropriate ternary relational postulates. Each logic L gives rise to a Calculus of L -theories, on which particular candidate logical axioms have the combinatorial properties expected from the well-known Curry–Howard isomorphism (with improvements by Dezani and her fellow intersection type theorists.). We apply their bubbling lemma, updating the Fools Model of Combinatory Logic at the pure → level for the system B ∧ T . We make fusion ∘ an explicit connective, proving a combinator correspondence theorem. Having taken relevant → as a left residual for ∘, we explore its right residual mate → r . Finally we concentrate on and prove a finite model property for the classical minimal relevant logic CB , a conservative extension of the minimal positive relevant logic B + .

We use intersection types as a tool for obtaining λ-models. Relying on the notion of easy intersection type theory, we successfully build a λ-model in which the interpretation of an arbitrary simple easy term is any filter which can be described by a continuous predicate. This allows us to prove two results. The first gives a proof of consistency of the λ-theory where the λ-term (λx.xx)(λx.xx) is forced to behave as the join operator. This result has interesting consequences on the algebraic structure of the lattice of λ-theories. The second result is that for any simple easy term, there is a λ-model, where the interpretation of the term is the minimal fixed point operator.

We present a new system of intersection types for a composition-free calculus of explicit substitutions with a rule for garbage collection, and show that it characterizes those terms which are strongly normalizing. This system extends previous work on the natural generalization of the classical intersection types system, which characterized head normalization and weak normalization, but was not complete for strong normalization. An important role is played by the notion of available variable in a term, which is a generalization of the classical notion of free variable.

This paper defines reduction on derivations in the strict intersection type assignment system of [2], by generalising cutelimination, and shows a strong normalisation result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterisation of normalisability using intersection types.

We provide a new and elementary proof of strong normalization for the lambda calculus of intersection types. It uses no strong method, like for instance Tait-Girard reducibility predicates, but just simple induction on type complexity and derivation length and thus it is obviously formalizable within first order arithmetic. To obtain this result, we introduce a new system for intersection types whose rules are directly inspired by the reduction relation. Finally, we show that not only the set of strongly normalizing terms of pure lambda calculus can be characterized in this system, but also that a straightforward modification of its rules allows to characterize the set of weakly normalizing terms.

Recent work on infinitary versions of the lambda calculus has shown that the infinite lambda calculus can be a useful tool to study the unsolvable terms of the classical lambda calculus. Working in the framework of the intersection type disciplines, we devise a type assignment system such that two terms are equal in the infinite lambda calculus iff they can be assigned the same types in any basis. A novel feature of the system is the presence of a type constant to denote the set of all terms of order zero, and the possibility of applying a type to another type. We prove a completeness and an approximation theorem for our system. Our results can be considered as a first step towards the goal of giving a denotational semantics for the lambda calculus which is suited for the study of the unsolvable terms. However, some noncontinuity phenomena of the infinite lambda calculus make a full realization of this idea (namely the construction of a filter model) a quite difficult task.

International audience; 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.

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 lambdal-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 lambda-terms, LambdaJ-terms (lambda-terms with generalised application), and lambdax-terms (lambda-terms with explicit substitution). We explain via our system why the type systems iin the natural deduction format for LambdaJ and lambdax known from the literature contain extra, exceptional rules for typing generalised application or substitution; and we show a new characterisation of the beta-strongly normalising l-terms, as a corollary to a PSN-result, relating the lambda-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 beta-strongly normalising lambda-terms in terms of assignment of strict types follows as an easy corollary of our results., Fundação para a Ciência e Tecnologia

International audience; We propose intersection type assignment systems for two resource control term calculi: the lambda calculus and the sequent lambda calculus with explicit operators for weakening and contraction. These resource control calculi, /\® and /\®-Gtz, respectively, capture the computational content of intuitionistic natural deduction and intuitionistic sequent logic with explicit structural rules. Our main contribution is the characterisation of strong normalisation of reductions in both calculi. We first prove that typability implies strong normalisation in /\® by adapting the reducibility method. Then we prove that typability implies strong normalisation in /\®-Gtz by using a combination of well-orders and a suitable embedding of /\®-Gtz-terms into /\®-terms which preserves types and enables the simulation of all its reductions by the operational semantics of the /\®-calculus. Finally, we prove that strong normalisation implies typability in both systems using head subject expansion.

International audience; The study of type isomorphisms for different λ-calculi started over twenty years ago, and a very wide body of knowledge has been established, both in terms of results and in terms of techniques. A notable missing piece of the puzzle was the characterization of type isomorphisms in the presence of intersection types. While, at first thought, this may seem to be a simple exercise, it turns out that not only finding the right characterization is not simple, but that the very notion of isomorphism in intersection types is an unexpectedly original element in the previously known landscape, breaking most of the known properties of isomorphisms of the typed λ-calculus. In particular, isomorphism is not a congruence and types that are equal in the standard models of intersection types may be nonisomorphic.

A model characterising strong normalisation for Klop's extension of λ-calculus is presented. The main technical tools for this result are an inductive definition of strongly normalising terms of Klop's calculus and an intersection type system for terms of Klop's calculus.

International audience; In this paper we show that the membership problem for second order non- linear Abstract Categorial Grammars is decidable. A consequence of that result is that Montague-like semantics yield to a decidable text generation problem. Furthermore the proof we propose is based on a new tool, Higher Order Intersection Signatures, which grasps statically dynamic properties of λ-terms and presents an interest in its own.

We show how to use intersection types for building models of a λ-calculus enriched with recursive terms, whose intended meaning is of minimal fixed points. As a by-product we prove an interesting consistency result.

This paper defines reduction on derivations (cut-elimination) in the Strict Intersection Type Assignment System of an earlier paper and shows a strong normalization result for this reduction. Using this result, new proofs are given for the approximation theorem and the characterization of normalizability of terms using intersection types.

We construct two inverse limit λ-models which completely characterise sets of terms with similar computational behaviours: the sets of normalising, head normalising, weak head normalising λ-terms, those corresponding to the persistent versions of these notions, and the sets of closable, closable normalising, and closable head normalising λ-terms. More precisely, for each of these sets of terms there is a corresponding element in at least one of the two models such that a term belongs to the set if and only if its interpretation (in a suitable environment) is greater than or equal to that element. We use the finitary logical description of the models, obtained by defining suitable intersection type assignment systems, to prove this.

The invariance of the meaning of a λ-term by reduction/expansion w.r.t. the considered computational rules is one of the minimal requirements for a λ-model. Being the intersection type systems a general framework for the study of semantic domains for the Lambdacalculus, the present paper provides a characterisation of “meaning invariance” in terms of characterisation results for intersection type systems enabling typing invariance of terms w.r.t. various notions of reduction/expansion, like β, η and a number of relevant restrictions of theirs.

We characterize those type preorders which yield complete intersection-type assignment systems for λ-calculi, with respect to the three canonical set-theoretical semantics for intersection-types: the inference semantics, the simple semantics, and the F-semantics. These semantics arise by taking as interpretation of types subsets of applicative structures, as interpretation of the preorder relation , ≤, set-theoretic inclusion, as interpretation of the intersection constructor , ∩, set-theoretic intersection, and by taking the interpretation of the arrow constructor , → à la Scott, with respect to either any possible functionality set , or the largest one, or the least one.These results strengthen and generalize significantly all earlier results in the literature, to our knowledge, in at least three respects. First of all the inference semantics had not been considered before. Second, the characterizations are all given just in terms of simple closure conditions on the preorder relation , ≤, on the types, rather than on the typing judgments themselves. The task of checking the condition is made therefore considerably more tractable. Last, we do not restrict attention just to λ-models, but to arbitrary applicative structures which admit an interpretation function. Thus we allow also for the treatment of models of restricted λ-calculi. Nevertheless the characterizations we give can be tailored just to the case of λ-models.

In this paper we present two non-standard-type inference systems for conjunctive strictness and totality analyses of higher-order-typed functional programs and prove completeness results for both the strictness and the totality-type entailment relations. We also study the interactions between strictness and totality analyses, showing that the information obtainable by a system that combines the two analyses, even though more refined than the information given by the two separate systems, cannot be effectively used. A main feature of our approach is that all the results are proved by relying directly on the operational semantics of the programming language considered. This leads to a rather direct presentation which involves relatively little mathematical overhead. Copyright 2002 Elsevier Science B.V.

We define the typed lambda calculus Fω∧ (F-omega-meet), a natural generalization of Girard's system Fω (F-omega) with intersection types and bounded polymorphism. A novel aspect of our presentation is the use of term rewriting techniques to present intersection types, which clearly splits the computational semantics (reduction rules) from the syntax (inference rules) of the system. We establish properties such as Church-Rosser for the reduction relation on types and terms, and strong normalization for the reduction on types. We prove that types are preserved by computation (subject reduction), and that the system satisfies the minimal types property. We define algorithms for type checking and subtype checking. The development culminates with the proof of decidability of typing in Fω∧, containing the first proof of decidability of subtyping of a higher-order lambda calculus with subtyping.

We characterize β-strongly normalizing λ-terms by means of a non-idempotent intersection type system. More precisely, we first define a memory calculus K together with a non-idempotent intersection type system K, and we show that a K-term t is typable in K if and only if t is K-strongly normalizing. We then show that β-strong normalization is equivalent to K-strong normalization. We conclude since λ-terms are strictly included in K-terms.

Inferring types for polymorphic recursive function definitions (abbreviated to polymorphic recursion) is a recurring topic on the mailing lists of popular typed programming languages. This is despite the fact that type inference for polymorphic recursion using ∀-types has been proved undecidable. This report presents several programming examples involving polymorphic recursion and determines their typability under various type systems, including the Hindley-Milner system, an intersection-type system, and extensions of these two. The goal of this report is to show that many of these examples are typable using a system of intersection types as an alternative form of polymorphism. By accomplishing this, we hope to lay the foundation for future research into a decidable intersection-type inference algorithm.We do not provide a comprehensive survey of type systems appropriate for polymorphic recursion, with or without type annotations inserted in the source language. Rather, we focus on examples for which types may be inferred without type annotations, with an emphasis on systems of intersection- types.

Light Affine Lambda Calculus is a term calculus for polynomial time computation ([K. Terui. Light affine lambda calculus and polytime strong normalization. In Proceedings of LICS'01, pages 209–220, 2001]). Some of the terms of Light Affine Lambda Calculus must however be regarded as errors. Intuitionistic Light Affine Logic (ILAL) types only terms without errors, but not all of them. We introduce two type assignment systems with intersection types : in the first one, typable pseudo-terms are exactly the terms without errors ; in the second one, they are exactly those that reduce to normal terms without errors.

We introduce a new unification procedure for the type inference problem in the intersection type discipline. It is well known that type inference in this case should succeed exactly for the strongly normalizing expressions. We give a proof for the strong normalization result in the intersection type discipline, which we obtain by putting together some well-known results and proof techniques. Our proof uses a variant of Klop’s extended λ-calculus, for which it is shown that strong normalization is equivalent to weak normalization. This is proved here by means of a finiteness of developments theorem, obtained following de Vrijer’s combinatory technique. The main property of this extended calculus is uniformity, i.e. weak and strong normalizabilities coincide. The strong normalizability result is therefore a consequence of the fact, first established by Coppo and Dezani (for the λ-calculus) that typability implies weak normalizability. We then show that the unification process which is the basis for type inference exactly corresponds to reduction in the extended λ-calculus. Finally we show that our notion of unification allows us to compute a principal typing for any typable λ-expression.

The lazy evaluation of the λ-calculus, both in call-by-name and in call-by-value setting, is studied. Starting from a logical descriptions of two topological models of such calculi, a pre-order relation on terms, stratified by types, is defined, which grasps exactly the two operational semantics we want to model. Such a relation can be used for building two fully abstract models.

We show how to characterise compositionally a number of evaluation properties of λ-terms using Intersection Type assignment systems. In particular, we focus on termination properties, such as strong normalisation, normalisation, head normalisation, and weak head normalisation. We consider also the persistent versions of such notions. By way of example, we consider also another evaluation property, unrelated to termination, namely reducibility to a closed term.Many of these characterisation results are new, to our knowledge, or else they streamline, strengthen, or generalise earlier results in the literature.The completeness parts of the characterisations are proved uniformly for all the properties, using a set-theoretical semantics of intersection types over suitable kinds of stable sets. This technique generalises Krivine's and Mitchell's methods for strong normalisation to other evaluation properties.

We introduce a type assignment system which is parametric with respect to five families of trees obtained by evaluating λ-terms (Bhm trees, Lvy-Longo trees, etc.). Then we prove, in an (almost) uniform way, that each type assignment system fully describes the observational equivalences induced by the corresponding tree representation of λ-terms. More precisely, for each family of trees, two λ-terms have the same tree if and only if they get assigned the same types in the corresponding type assignment system. Copyright 2002, Elsevier Science B.V.

Intersection types discipline allows to define a wide variety of models for the type free lambda-calculus, but the Curry–Howard isomorphism breaks down for this kind of type systems. In this paper we show that the correspondence between types and suitable logical formulas can still be recovered appealing to the fact that there is a strict connection between the semantics for lambda-calculus induced by the intersection types and a Kripke-style semantics for modal and relevant logics. Indeed, we present a modal logic hinted by the analysis of the sub-typing relation for intersection types, and we show that the deduction relation for such a modal system is a conservative extension of the relation of sub-typing. Then, we define a Kripke-style semantics for the formulas of such a system, present suitable sequential calculi, prove a completeness theorem and give a syntactical proof of the cut elimination property. Finally, we define a decision procedure for theorem-hood and we show that it yields the finite model property and cut-redundancy.

This paper studies normalization of typeable terms and the relation between approximation semantics and filter models for Combinator Systems. It presents notions of approximants for terms, intersection type assignment, and reduction on type derivations; the last will be proved to be strongly normalizable. With this result, it is proved that every typeable term has an approximant with the same type, and a characterization of the normalization behaviour of terms using their assignable types is given. Then the two semantics are defined and compared, and it is shown that the approximants semantics is fully abstract but the filter semantics is not.