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

Confluence properties of weak and strong calculi of explicit substitutions

Abstract : Categorical combinators and more recently ls-calculus have been introduced to provide an explicit treatments of substitutions in the l-calculus. We reintroduce here the ingredients of these calculi in a self-contained and stepwise way, with a special emphasis on confluence properties. The main new results of the paper w.r.t. are the following : - we present a confluent weak calculus of substitutions, where no variable clashes can be feared - we solve a conjecture : ls-calculus is not confluent (it is confluent on ground terms only). This unfortunate result is "repaired" by presenting a confluent version of ls-calculus, named the lEnv-calculus called here the confluent ls-calculus.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Monday, May 29, 2006 - 5:16:10 PM
Last modification on : Thursday, February 3, 2022 - 11:16:40 AM
Long-term archiving on: : Friday, May 13, 2011 - 10:48:59 PM


  • HAL Id : inria-00077189, version 1



P.L. Curien, Thérèse Hardin, Jean-Jacques Levy. Confluence properties of weak and strong calculi of explicit substitutions. [Research Report] RR-1617, INRIA. 1992. ⟨inria-00077189⟩



Record views


Files downloads