The ∆-calculus: Syntax and Types

Luigi Liquori 1 Claude Stolze 1
1 KAIROS - Logical Time for Formal Embedded System Design
CRISAM - Inria Sophia Antipolis - Méditerranée , Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : We present the ∆-calculus, an explicitly typed λ-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories T , e.g. the Coppo-Dezani, the Coppo-Dezani-Sallé, the Coppo-Dezani-Venneri and the Barendregt-Coppo-Dezani ones, producing a family of ∆-calculi with related intersection typed systems. We prove the main properties like Church-Rosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction. We state the relationship between the intersection type assignment systems à la Curry and the corresponding intersection typed systems à la Church by means of an essence function translating an explicitly typed ∆-term into a pure λ-term one. We finally translate a ∆-term with type coercions into an equivalent one without them; the translation is proved to be coherent because its essence is the identity. The generic ∆-calculus can be parametrized to take into account other intersection type theories as the ones in the Barendregt et al. book.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

https://hal.archives-ouvertes.fr/hal-02190691
Contributeur : Claude Stolze <>
Soumis le : lundi 22 juillet 2019 - 16:34:19
Dernière modification le : mardi 20 août 2019 - 14:29:27

Fichier

delta.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-02190691, version 1

Collections

Citation

Luigi Liquori, Claude Stolze. The ∆-calculus: Syntax and Types. FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. ⟨hal-02190691⟩

Partager

Métriques

Consultations de la notice

94

Téléchargements de fichiers

26