From categorical combinators to lambda-sygma-calculi, a quest for confluence

Abstract : The l-calculus is known to be the theoretical base of functional programming languages. But, the substitution, which describes the parameters' passage, belongs only to the meta-language and this is a major drawback when dealing with compilation. Therefore, extensions of l-calculus, able to manipulate explicity substitutions and still confluent, are required. The categorical combinatory logic, introduced in 1983, and the ls-calculi, presented in 1988 and 1989, are responses to this question. We give here a survey of these theories, explaining their evolution from a confluence point of view. This report does not contain new results and remains rather informal, avoiding too technical details.
Type de document :
[Research Report] RR-1777, INRIA. 1992
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 29 mai 2006 - 11:50:59
Dernière modification le : vendredi 16 septembre 2016 - 15:19:38
Document(s) archivé(s) le : vendredi 13 mai 2011 - 22:34:10



  • HAL Id : inria-00077017, version 1



Thérèse Hardin. From categorical combinators to lambda-sygma-calculi, a quest for confluence. [Research Report] RR-1777, INRIA. 1992. 〈inria-00077017〉



Consultations de la notice


Téléchargements de fichiers