Séparation des couleurs dans un lambda-calcul bichrome

Résumé : Dans cet article nous introduisons un λ-calcul bichrome pour expliciter une partie de l'évaluation d'un terme en précisant la localité du calcul1. L'intérêt est alors de pouvoir définir une transformation, par β-expansion, qui regroupe les expressions de même couleur. Les propriétés de correction, de terminaison et de confluence de cette transformation sont démontrées 'a l'aide de l'assistant de preuves Coq. Cette transformation est indépendante de la sémantique de communication et de synchronisation de l'application. On s'intéresse alors aux applications utilisant deux unités de calcul comme les couples client-serveur de la programmation Web. Nous abordons le passage à un λ-calcul à plus de deux couleurs et montrons les difficultés que cela engendre.
Type de document :
Communication dans un congrès
JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00665958
Contributeur : Alain Monteil <>
Soumis le : vendredi 3 février 2012 - 11:55:44
Dernière modification le : mardi 13 septembre 2016 - 01:04:41
Document(s) archivé(s) le : vendredi 4 mai 2012 - 02:30:07

Fichier

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

Identifiants

  • HAL Id : hal-00665958, version 1

Collections

Citation

Emmanuel Chailloux, Bernard Serpette. Séparation des couleurs dans un lambda-calcul bichrome. JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012. 〈hal-00665958〉

Partager

Métriques

Consultations de la notice

212

Téléchargements de fichiers

148