ABSTRACT. Quantitative techniques are emerging in different areas of computer science, such as model checking, logic, and automata theory, to face the challenge of today's resource aware computation.

In this talk we give a clean theoretical understanding of the use of resources in quantitative systems, and we introduce different alternatives, suitable for a wide range of powerful models of computation, such as for example pattern matching, control operators and infinitary computations.

We survey some interesting results related to those typing systems such as:
(1) characterization of operational properties,
(2) computation of exact measures for reduction sequences and normal forms,
(3) inhabitation problems, and
(4) observational equivalence.

ABSTRACT. Refining and extending previous work by Retoré (1994), we develop a systematic approach to intersection types via natural deduction. We show how a step of beta reduction can be seen as performing, at the level of typing derivations, Prawitz reductions in parallel. Then we derive as immediate consequences of Subject reduction the main theorems about normalization for intersection types: for system D, strong normalization, for system DΩ, the leftmost reduction termination for terms typable without Ω.

ABSTRACT. A new proof of strong normalization for simple type assignment for λ-calculus is obtained, through a translation from this system to a system of uniform intersection types, which is equivalent to it as typability power and whose strong normalization property can be easily proved by induction on derivation.

ABSTRACT. We investigate the possibility of a semantic account of the execution time (i.e. the number of beta v-steps leading to the normal form, if any) for the shuffling calculus, an extension of Plotkin's untyped call-by-value lambda-calculus. For this purpose, we use a linear logic based denotational model that can be seen as a non-idempotent intersection type system: relational semantics. Our investigation is inspired by similar ones for linear logic proof-nets and untyped call-by-name lambda-calculus. We first prove a qualitative result: a (possibly open) term is normalizable for weak reduction (which does not reduce under abstractions) if and only if its interpretation is not empty. We then show that the size of type derivations can be used to measure the execution time. Finally, we show that, differently from the case of linear logic and call-by-name lambda-calculus, the quantitative information enclosed in type derivations does not lift to types (i.e. to the interpretation of terms). In order to get a genuine semantic measure of execution time in a call-by-value setting, we conjecture that a refinement of its syntax and operational semantics is needed.

ABSTRACT. Intersection types have been originally developed as an extension of 
simple types, but they can also be used for refining simple types. In this 
talk we concentrate on the latter option; more precisely, on the use of 
intersection types in the context of higher-order recursion schemes. 
Intersection types were used in this context for several purposes like 
model-checking, pumping, transformations of schemes, etc. After an 
overview, I will show how intersection types can be used to solve problems 
talking about unboundedness of some quantities. An example of such a 
problem is: given a higher-order recursion scheme generating an infinite 
tree, decide whether for every number n there is a path in this tree 
containing at least n occurrences of a fixed letter #. Notice that this is 
not a regular property of the tree, thus it cannot be decided using 
standard model-checking methods.

ABSTRACT. Gradual typing integrates dynamic and static types. Since its introduction, it has been successfully applied to several extensions of simple types, including subtyping, parametric polymorphism and substructural types. This work studies its application to intersection type systems. We introduce a new approach to define a gradual version of the original intersection type system of Coppo and Dezani. We then present a new operational semantics for terms typed with static and dynamic intersection types, which enables dynamic type casts and identifies the causes for type errors in a framework inspired by the blame calculus. Finally we prove several properties of our system including a correctness criteria and soundness of the extension of the original gradual type system.

ABSTRACT. We study the question of extending the BCD intersection type system with additional type constructors. On the typing side, we focus on adding the usual rules for product types. On the subtyping side, we consider a generic way of defining a subtyping relation on families of types which include intersection types. We find back the BCD subtyping relation by considering the particular case where the type constructors are intersection, omega and arrow. We obtain an extension of BCD subtyping to product types as another instance. We show how the preservation of typing by both reduction and expansion is satisfied in all the considered cases. Our approach takes benefits from a ``sub-formula property'' of the proposed presentation of the subtyping relation.

ABSTRACT. In his paper introducing linear logic, Girard briefly mentioned how full linear logic could be seen, in an informal sense, as the limit of its purely linear fragment.  Several ways of expanding and formalizing this idea have been developed through the years, including what I call polyadic approximations.  In this talk, I will show how these are deeply related to intersection type systems, via a general construction that is sufficiently broad to allow recovering every well known intersection type system and their normalization properties, as well as introducing new type systems in wildly disparate contexts, with applications ranging from deadlock-freedom in the pi-calculus to a type-theoretic proof of the Cook-Levin theorem.  

(Part of this work was developed jointly with Luc Pellissier and Pierre Vial).