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 <>
Submitted on : Monday, May 29, 2006 - 11:50:59 AM
Last modification on : Thursday, February 11, 2021 - 2:50:07 PM
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