%\subsection{Strictness}

Church original definition of (untyped)  $\l$-terms \cite{Church41} has this 
clause for abstraction:
\begin{center}
If $M\in\Lambda_{I}$ and $x\in FV(M)$, then $\lx M\in\Lambda_{I}$.
\end{center}
\ie in this language there cannot be vacuous abstractions.  The only 
difference between $\Lambda_{I}$ and $\Lambda$ is the lack of 
$\mathbf{K}$.  Indeed every term in $\Lambda$ can be defined from 
$\Lambda_{I}$ and $\mathbf{K}$.  The $\l\ I$-calculus is the theory of 
conversion restricted to those terms.  This fragment was favored by 
Church over the usual calculus, because, among other issues, it is 
strong enough to represent every partial recursive functions, albeit 
not in the most efficient way: see \cite{Barendregt80} Chapter 
$2.2.2-2.2.5$ and more extensively in Chapter $9$.  See 
\cite{Gabbay92}for an historical account.  Its combinator counterpart 
obviously excludes $\mathbf{K}$ and consists of $\mathbf{I,S,B, C}$, 
see \cite{Curry58} and \cite{Barendregt80}, Appendix B.

This would correspond in a simply-typed setting to admitting 
\emph{only} strict types: more formally if we denote with 
$\Lambda^{\GImp{k}}$ the terms typable in a Curry- system based on the 
$\GImp{k}$ function space, then $\Lambda^{\GImp{1}}= 
\Lambda^{\GImp{u}}\cap \Lambda_{I}$, as noted for example in 
\cite{BakerFinch94}.

On an other front, the relevance logic project emerged in the early 
sixties out of Anderson and Belnap's dissatisfaction with the 
so-called `paradoxes of implication', let it be material, 
intuitionistic or strict, was built on the work of Moh, Church, Parry 
in the fifties\footnote{Some early work in the twenties in the Soviet 
Union was, at the time, not accessible.} and climaxed with the 
publication of the first volume of \emph{Entailment} \cite{Anderson75}.  
Following Girard's and Belnap's \cite{SH?} suggestion we will 
\emph{not} refer to this calculus as \emph{strict} logic, as the 
former may also satisfy other principles such as distributivity of 
arrow over conjunction.

On a unrelated front, starting with Mycroft's seminal paper 
\cite{Mycroft80}, compile-time analysis of functional programs zeroed 
on strictness and sharing analysis first in terms of abstract 
interpretation, later by using types to represent those ` intensional' 
information about functions.  However, earlier works, as \cite{Kuo89} 
used non-standard primitive type to distinguish strict or non-strict 
terms, closed only under intuitionistic implication.  Not forgetting 
Wadler's early paper \cite{Wadler90} on linear logic and sharing 
analysis, Wright \cite{Wright91,Wright92} (see also 
\cite{BakerFinch94}) seems the first one to have extended the 
Curry-Howard isomorphism to (the implicational fragment of ) relevant 
logic and connected the two areas

\begin{metanote} Insert a comparison of those systems to ours.
\end{metanote}
