HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Monday, May 29, 2006 - 11:50:59 AM
Last modification on : Friday, February 4, 2022 - 3:18:30 AM
Long-term archiving on: : Friday, May 13, 2011 - 10:34:10 PM


  • 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⟩



Record views


Files downloads