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.
There is a video of the talk.
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.
Modular pre-processing for automated reasoning in dependent type theory, with V. Blot, D. Cousineau, Enzo Crance, L. Dubois de Prisque, C. Keller, A. Mahboubi. Abstract: The power of modern automated theorem provers can be put at the service of interactive theorem proving. But this requires in particular bridging the expressivity gap between the logics these provers are respectively based on. This paper presents the implementation of a modular suite of pre-processing transformations, which incrementally bring certain formulas expressed in the Calculus of Inductive Constructions closer to the first-order logic of Satifiability Modulo Theory solvers. These transformations address issues related to the axiomatization of inductive types, to polymorphic definitions or to the different implementations of a same theory signature. This suite is implemented as a plugin for the Coq proof assistant, and integrated to the SMTCoq toolchain.
Sequences and infinitary intersection types.
We introduce a new representation of non-idempotent intersection types, using sequences (families indexed with natural numbers) instead of lists or multisets. This allows scaling up intersection type theory to the infinitary λ-calculus.
We thus characterize hereditary head normalization.
On our way, we use non-idempotent
intersection to retrieve some well-known results on infinitary terms.
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.