Types intersections non-idempotents pour raffiner la normalisation forte avec des informations quantitatives

Abstract : We study systems of non-idempotent intersection types for different variants of the lambda-calculus and we discuss properties and applications. Besides the pure lambda-calculus itself, the variants are a λ-calculus with explicit substitutions and a lambda-calculus with constructors, matching and a fixpoint operator. The typing systems we introduce for these calculi all characterize strongly normalising terms. But we also show that, by dropping idempotency of intersections, typing a term provides quantitative information about it: a trivial measure on its typing tree gives a bound on the size of the longest beta-reduction sequence from this term to its normal form. We explore how to refine this approach to obtain finer results: some of the typing systems, under certain conditions, even provide the exact measure of this longest beta-reduction sequence, and the type of a term gives information on the normal form of this term. Moreover, by using filters, these typing systems can be used to define a denotational semantics.
Complete list of metadatas

Cited literature [36 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/tel-01099657
Contributor : Alexis Bernadet <>
Submitted on : Monday, January 5, 2015 - 9:10:18 AM
Last modification on : Wednesday, March 27, 2019 - 4:41:27 PM
Long-term archiving on : Wednesday, June 3, 2015 - 1:05:44 PM

Identifiers

  • HAL Id : tel-01099657, version 1

Collections

Citation

Alexis Bernadet. Types intersections non-idempotents pour raffiner la normalisation forte avec des informations quantitatives. Langage de programmation [cs.PL]. Ecole Doctorale Polytechnique, 2014. Français. ⟨tel-01099657⟩

Share

Metrics

Record views

261

Files downloads

162