| Author | Title | Key Words | Abstract |
|---|---|---|---|
| Ferruccio Damiani | Conjunctive Types and Useless-Code Elimination | non-standard type inference, program analysis, useless-code | We investigate the use of conjunctive non-standard type inference for the elimination of useless-code in higher-order typed functional programs. Useless-code elimination can be performed by optimizing compilers to improve the quality of the code produced. This kind of optimization is particularly useful when dealing with programs obtained by automatic translation from constructive proofs. |
| Grzegorz Grudzinski | A Minimal System of Disjunctive Properties for Strictness Analysis | intersection types, union types, program analysis, strictness analysis, abstract interpretation | In this paper we study a simple disjunctive system for strictness analysis. The paper gives a definition of the system (an abstract interpretation and an equivalent inference system) and investigates its properties. This system is minimal in a certain sense and has several important features (we prove polymorphic invariance, optimal interpretations of constants; these are the first proofs of these properties for a system with disjunctions). Also it is more tractable than other methods for disjunctive analysis of programs which were proposed so far. Moreover the way we define the system is similar enough to more traditional abstract interpretations that the standard algorithms for computing program properties can be used here, which does not seem to be the case with the other, more complicated techniques. |
| Fabio Alessi, Mariangiola Dezani-Ciangaglini, and Furio Honsell | A Complete Characterization of the Complete Intersection-Type Theories | We characterize those intersection type theories
which yield complete intersection type assignment
systems for $\lambda$-calculi, with respect to the three
canonical set-theoretical semantics for intersection
types: the inference semantics, the simple semantics and
the F-semantics.
These are those semantics which arise by taking as interpretation of the intersection operator, $\bigcap$, set-theoretic inclusion, and by taking the interpretation of the arrow constructor, $\Rightarrow$, à la Scott, with respect to any possible functionality set, the maximal 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. Secondly the characterizations are all given just in terms of simple closure conditions on the preorder relation, $\leq$, on types, rather than on the typing judgements themselves. The task of checking the condition is made therefore considerably more tractable. Lastly we do not restrict attention just to $\lambda $-models, but to arbitrary applicative structures which admit an interpretation function. Thus we allow also for the treatment of models of restricted $\lambda$-calculi, nevertheless the characterizations we give can be tailored just to the case of $\lambda$-models. | |
| Silvia Ghilezan | Intersection Types and Topologies in Lambda Calculus (abstract to appear in proceedings) (full paper not to appear in proceedings) | Topologies are introduced on the set of lambda terms by their typeability in the full intersection type assignment system. These topologies give rise to simple proofs of some fundamental results of the lambda calculus such as the Continuity Theorem and the Genericity Lemma. We show that application is continuous, unsolvable terms are bottoms and normal forms are isolated points with respect to these topologies. The restriction of all these topologies to the set of closed lambda terms appears to be unique. We compare the introduced topology with the filter topology on the set of (closed) lambda terms and show that they coincide. | |
| Trevor Jim | A Polar Type System | We introduce a restriction of the type system of intersection types and universal type quantification, in which quantifiers must only appear at positive occurrences in types, and intersections at negative occurrences. We show that the system is an extension of the system of rank two intersection types, and, therefore, of ML. The system is much more powerful than ML; for example, all pure normal forms are typable in the system. We show that the system has principal pairs, and that type inference for the system is decidable. These properties are retained when the system is extended by a form of polymorphic recursion. | |
| Robert K. Meyer | What Entailment Can Do for Type Theory | entailment, intersection types, union types, depth relevance, prime theory, negation, Boolean, B+, CB | Logics of entailment were developed for philosophical reasons before recent work in type theory. Yet there is a confluence between them. This confluence is evident in the logic B+, which was proposed in 1972 as the minimal relevant logic. Yet a few years later an essentially equivalent system was independently invented as a theory of (non-Curry) intersection (and union) types. This paper suggests several ways in which research in relevant logic can be adapted to produce results (and perhaps even insights) for type-theorists. Conversely the profound technical understanding that has produced filter models for functional theories definitively illumines the semantics of relevant logics. |
| Ralph Matthes | Characterizing Strongly Normalizing Terms for a Lambda Calculus with Generalized Applications via Intersection Types | intersection types, strong normalization, permutative conversions, saturated sets | An intersection type assignment system for the extension LambdaJ of the untyped lambda-calculus, introduced by Joachimski and Matthes, is given and proven to characterize the strongly normalizing terms of LambdaJ. Since LambdaJ's generalized applications naturally allow permutative/commuting conversions, this the first analysis of a term rewrite system with permutative conversions by help of intersection types. Two proofs are given for the fact that the typable terms are strongly normalizing: One by the computability predicates method a la Tait and one showing directly that strongly normalizing typable terms are closed under (generalized) application and substitution. It is also shown that a straightforward extension of the type assignment for lambda calculus fails to capture the strongly normalizing terms. |