Search

Abstract:  We consider semantics for the class-based object-oriented calculus Featherweight Java (without casts) based upon approximation. We also define an intersection type assignment system for this calculus and show that it satisfies subject reduction and expansion, i.e. types are preserved under reduction and its converse. We establish a link between type assignment and the approximation semantics by showing an approximation result, which leads to a sufficient condition for the characterisation of head-normalisation and termination.  We show the expressivity of both our calculus and our type system by defining an encoding of Combinatory Logic into our calculus and showing that this encoding preserves typeability. We also show that our system characterises the normalising and strongly normalising terms for this encoding. We thus demonstrate that the great analytic capabilities of intersection types can be applied to the context of class-based object orientation. [Copyright &y& Elsevier]

We present a typing system with non-idempotent intersection types, typing a term syntax covering three different calculi: the pure λ-calculus, the calculus with explicit substitutions λS, and the calculus with explicit substitutions, contractions and weakenings λlxr. In each of the three calculi, a term is typable if and only if it is strongly normalising, as it is the case in (many) systems with idempotent intersections. Non-idempotency brings extra information into typing trees, such as simple bounds on the longest reduction sequence reducing a term to its normal form. Strong normalisation follows, without requiring reducibility techniques. Using this, we revisit models of the λ-calculus based on filters of intersection types, and extend them to λS and λlxr. Non-idempotency simplifies a methodology, based on such filter models, that produces modular proofs of strong normalisation for well-known typing systems (e.g. System F). We also present a filter model by means of orthogonality techniques, i.e. as an instance of an abstract notion of orthogonality model formalised in this paper and inspired by classical realisability. Compared to other instances based on terms (one of which rephrases a now standard proof of strong normalisation for the λ-calculus), the instance based on filters is shown to be better at proving strong normalisation results for λS and λlxr. Finally, the bounds on the longest reduction sequence, read off our typing trees, are refined into an exact measure, read off a specific typing tree (called principal ); in each of the three calculi, a specific reduction sequence of such length is identified. In the case of the λ-calculus, this complexity result is, for longest reduction sequences, the counterpart of de Carvalho's result for linear head-reduction sequences. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

We present a general theorem capturing conditions required for the termination of abstract reduction systems. We show that our theorem generalises another similar general theorem about termination of such systems. We apply our theorem to give interesting proofs of termination for typed combinatory logic. Thus, our method can handle most path-orderings in the literature as well as the reducibility method typically used for typed combinators. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. All proofs have been formally machine-checked in Isabelle/HOL. [ABSTRACT FROM AUTHOR]

Abstract: This paper gives a new proof for the approximation theorem and the characterisation of normalisability using intersection types for a system with 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. [Copyright &y& Elsevier]

In this paper, we consider the typed versions of the λ-calculus written in a notation which helps describe canonical forms more elegantly than the classical notation, and enables to divide terms into classes according to their reductional behaviour. In this notation, β-reduction can be generalised from a relation on terms to one on equivalence classes. This class reduction covers many known notions of generalised reduction. We extend the Barendregt cube with our class reduction and show that the subject reduction property fails but that this is not unique to our class reduction. We show that other generalisations of reduction (such as the σ-reduction of Regnier) also behave badly in typed versions of the λ-calculus. Nevertheless, solution is at hand for these generalised reductions by adopting the useful addition of definitions in the contexts of type derivations. We show that adding such definitions enables the extensions of type systems with class reduction and σ-reduction to satisfy all the desirable properties of type systems, including subject reduction and strong normalisation. Our proposed typing relation ⊫c is the most general relation in the literature that satisfies all the desirable properties of type systems. We show that classes contain all the desirable information related to a term with respect to typing, strong normalisation, subject reduction, etc. [Copyright &y& Elsevier]

We introduce a typed π-calculus where strong normalisation is ensured by typability. Strong normalisation is a useful property in many computational contexts, including distributed systems. In spite of its simplicity, our type discipline captures a wide class of converging name-passing interactive behaviour. The proof of strong normalisability combines methods from typed λ-calculi and linear logic with process-theoretic reasoning. It is adaptable to systems involving state, non-determinism, polymorphism, control and other extensions. Strong normalisation is shown to have significant consequences, including finite axiomatisation of weak bisimilarity, a fully abstract embedding of the simply typed λ-calculus with products and sums and basic liveness in interaction. Strong normalisability has been extensively studied as a fundamental property in functional calculi, term rewriting and logical systems. This work is one of the first steps to extend theories and proof methods for strong normalisability to the context of name-passing processes. [Copyright &y& Elsevier]

We define display calculi for nominal tense logics extending the minimal nominal tense logic (MNTL) by addition of primitive axioms. To do so, we use the natural translation ofMNTL into the minimal tense logic of inequality (L≠) which is known to be properly displayable by application of Kracht's results. The rules of the display calculus δMNTL for MNTL mimic those of the display calculus δL≠ for L≠. We show that every MNTL‐valid formula admits a cut‐free derivation in δMNTL. We also show that a restricted display calculus δ−MNTL, is not only complete for MNTL, but that it enjoys cut‐elimination for arbitrary sequents. Finally, we give a weak Sahlqvist‐type theorem for two semantically defined extensions of MNTL. Using Kracht's techniques we obtain sound and complete display calculi for these two extensions based upon δMNTL and δ−MNTL respectively. The display calculi based upon δMNTL enjoy cut‐elimination for valid formulae only, but those based upon δ−MNTL enjoy cut‐elimination for arbitrary sequents. [ABSTRACT FROM PUBLISHER]

We present an algebraic framework that provides a general notion of recursive types. We characterize those type systems that guarantee the subject reduction property. Finally, we prove a strong normalization and a principle typing result. [ABSTRACT FROM AUTHOR]