Persistent and Consuming Types for Classical Logic [LiCS'20] (joint work with Delia Kesner) We use a non-idempotent intersection and union type system to capture exact measures of evaluation in the λμ-calculus. These exact measures correspond to the number of evaluation steps needed to obtain the normal form, and the size of this normal form. The λμ-calculus is a computational interpretation of classical natural deduction. We improve and extend previous works giving exact measures in the λ-calculus. Three evalutation strategies are considered: the head, the leftmost-outermost and the maximal strategies, the last one computing a longest reduction sequence and being associated to strong normalization.
Sequence Types for Hereditary Permutators [FSCD'19] The invertible terms in Scott’s model are known as the hereditary permutators. Equivalently, they are terms which are invertible up to βη-conversion with r spect to the composition of the λ-terms. Finding a type-theoretic characterizat on to the set of hereditary permutators was problem # 20 of TLCA list of problems. In 2008, Tatsuta proved that this was not possible with an inductive type system. Building on previous work, we use an infinitary intersection type system b sed on sequences (i.e., families of types indexed by integers) to characterize ereditary permutators with a unique type. This gives a positive answer to the problem in the coinductive case.
Non-Idempotent Types for Classical Calculi in Natural Deduction Style [LMCS, with Delia Kesner]
We define two resource aware typing systems for the λμ-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the lengths of the head-reduction and the maximal reduction sequences to normal form.
In the second part of this paper, the λμ-calculus is refined to a small-step calculus called λμs , which is inspired by the substitution at a distance paradigm. The λμs-calculus turns out to be compatible with a natural extension of the non-idempotent interpretations of λμ, i.e., λμs -reduction preserves and decreases typing derivations in an extended appropriate typing system. We thus derive a simple arithmetical characterization of strongly λμs -normalizing terms by means of typing.
Every term is meaningful in the infinitary relation model [LiCS'18] Infinite types and formulas are known to have really curious and unsound behaviors. For instance, they allow to type Omega, the auto-autoapplication and they thus do not ensure any form of normalization/productivity. Moreover, in most infinitary frameworks, it is not difficult to define a type R that can be assigned to every lambda-term. However, these observations do not say much about what coinductive (i.e. infinitary) type grammars are able to provide: it is for instance very difficult to know what types (besides $R$) can be assigned to a given term in this setting. We begin with a discussion on the expressivity of different forms of infinite types.
%We see that the non-idempotent intersection types, whose resource-awareness makes them the good framework to study infinitary typing.
Then, using the resource-awareness of sequential intersection types (system S) and tracking, we prove that infinite types are able to characterize the arity of every lambda-term and that, in the infinitary extension of the relational model, every term has a ``meaning'' i.e. a non-empty denotation. From the technical point of view, we must deal with the total lack of guarantee of productivity for typable terms: we do so by importing methods inspired by first order model theory.
Polyadic Approximations, Fibrations and Intersection Types [POPL'18, with Damiano Mazza and Luc Pellissier]:
Starting from an exact correspondence between linear approximations and non-idempotent intersection types, we develop a general framework for building systems of intersection types characterizing normalization properties. We show how this construction, which uses in a fundamental way Melliès and Zeilberger’s “type systems as functors” viewpoint, allows us to recover equivalent versions of every well known intersection type system (including Coppo and Dezani’s original system, as well as its non-idempotent variants independently introduced by Gardner and de Carvalho). We also show how new systems of intersection types may be built almost automatically in this way.
Types as Resources for Classical Natural Deduction [FSCD'17, with Delia Kesner]:
Abstract: We define two resource aware typing systems for the λ μ -calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments - based on decreasing measures of type derivations– to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the length of head-reduction sequences and maximal reduction sequences.
A longer version of this paper is available on Delia's page.
Reduction paths without permutations, or the expressive power of sequence types (outdated long (05.10.2017) version here). Abstract: The derivations of System S, whose intersection types are sequential, naturally collapses on R, the coinductive version of Gardner/de Carvalho's quantitive type system, featuring multisets as intersection type. We prove that this collapse is surjective : every derivation of R is the collapse of a derivation of S and we prove that we can capture every reduction path.