%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "curienhl96.ltx",
%%%     date      = "7 June 1996",
%%%     time      = "13:44:11 EDT",
%%%     author    = "David M. Jones",
%%%     email     = "jacm@theory.lcs.mit.edu",
%%%     url       = "http://theory.lcs.mit.edu/~jacm/",
%%%     address   = "Journal of the ACM
%%%                  MIT Laboratory for Computer Science
%%%                  Room NE43-316
%%%                  545 Technology Square
%%%                  Cambridge, MA 02139
%%%                  USA",
%%%     telephone = "(617) 253-5936",
%%%     FAX       = "(617) 253-3480",
%%%     checksum  = "45541 115 468 4066",
%%%     codetable = "ISO/ASCII",
%%%     supported = "yes",
%%%     docstring = "Copyright (c) 1995 by ACM, Inc.
%%%                  Permission to make digital or hard copies of part
%%%                  or all of this work for personal or classroom use
%%%                  is granted without fee provided that copies are
%%%                  not made or distributed for profit or direct
%%%                  commercial advantage and that copies bear this
%%%                  notice and the full citation on the first page.
%%%                  Copyrights for components of this work owned by
%%%                  others than ACM must be honored. Abstracting with
%%%                  credit is permitted. To copy otherwise, to
%%%                  republish, to post on servers, or to redistribute
%%%                  to lists, requires prior specific permission
%%%                  and/or a fee. Request permissions from
%%%                  Publications Dept, ACM Inc., fax +1 (212)
%%%                  869-0481, or permissions@acm.org.
%%%
%%%                  This is a LaTeX2e file.  To process it, you will
%%%                  need a copy of the acmabs document class, which is
%%%                  available via the following URL:
%%%
%%%                  http://theory.lcs.mit.edu/~jacm/acmart/acmabs.cls
%%%                  ",
%%%  }
%%% ====================================================================

\documentclass{acmabs}

\begin{document}

\Journal{Journal of the ACM}

\refkey{CurienHL96}

\title{Confluence Properties of Weak and Strong Calculi of Explicit
Substitutions}

\author{Pierre-Louis Curien \and Th{\'e}r{\`e}se Hardin \and
Jean-Jacques L{\'e}vy}

\Pages{362--397}

\Month{March}

\Year{1996}

\Volume{43}

\Number{2}

\maketitle

\begin{abstract}

Categorical combinators [Curien 1986/1993; Hardin 1989; Yokouchi 1989]
and more recently $\lambda\sigma$-calculus [Abadi 1991; Hardin and
L\'evy 1989], have been introduced to provide an explicit treatment of
substitutions in the $\lambda$-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 with respect to Curien [1986/1993], Harding [1989], Abadi
[1991], and Hardin and L\'evy [1989] are the following:
\begin{enumerate} \item We present a confluent weak calculus of
substitutions, where no variable clashes can be feared; \item We sove
a conjecture raised in Abadi [1991]: $\lambda\sigma$-calculus is not
confluent (it is confluent on ground terms only). \end{enumerate} This
unfortunate result is ``repaired'' by presenting a confluent version
of the $\lambda\sigma$-calculus, named the
$\lambda$\emph{Env}-calculus in Hardin and L\'evy [1989], called here
the confluent $\lambda\sigma$-calculus.

\end{abstract}

\begin{categories}

F.3.2 [\textbf{Logics and Meanings of Programs}]: Semantics of
Programming Languages---\emph{operational semantics}; F.3.3
[\textbf{Logics and Meanings of Programs}]: Studies of Program
Constructs---\emph{functional constructs}; F.4.1 [\textbf{Mathematical
Logic and Formal Languages}]: Mathematical Logic---\emph{lambda
calenders and related systems}

\end{categories}

\begin{terms}

Languages, Theory

\end{terms}

\begin{keywords}

Confluency, explicit substitutions

\end{keywords}

\end{document}
