Logical Combinators for Rich Type Systems

Pierre Genevès 1 Nabil Layaïda 1 Alan Schmitt 2
1 WAM - Web, adaptation and multimedia
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Résumé : Nous présentons une approche fonctionnelle pour concevoir des systèmes de types riches basée sur une représentation élégante et logique des types. La représentation n'est pas seulement propre, mais évite une augmentation exponentielle de la complexité en raison de duplication de sous-formules. Cela ouvre la voie pour résoudre un large éventail de problèmes tels que le sous-typage en temps simplement exponentiel, même si leur traduction directe dans la logique sous-jacente produit une explosion combinatoire de la taille de la formule, donnant une complexité en temps incorrectement présumée doublement exponentielle.
Type de document :
Rapport
[Research Report] RR-8010, INRIA. 2012, pp.18
Liste complète des métadonnées


https://hal.inria.fr/hal-00714353
Contributeur : Pierre Genevès <>
Soumis le : mercredi 4 juillet 2012 - 12:01:26
Dernière modification le : jeudi 9 février 2017 - 16:02:59
Document(s) archivé(s) le : vendredi 31 mars 2017 - 10:12:17

Fichier

RR-8010.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00714353, version 2

Citation

Pierre Genevès, Nabil Layaïda, Alan Schmitt. Logical Combinators for Rich Type Systems. [Research Report] RR-8010, INRIA. 2012, pp.18. <hal-00714353v2>

Partager

Métriques

Consultations de
la notice

658

Téléchargements du document

335