\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{lambda-calculus}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{the_calculus}{}\section*{{The $\lambda$-calculus}}\label{the_calculus}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{concepts}{Concepts}\dotfill \pageref*{concepts} \linebreak
\noindent\hyperlink{abstraction_and_application}{Abstraction and application}\dotfill \pageref*{abstraction_and_application} \linebreak
\noindent\hyperlink{evaluation_and_reduction}{Evaluation and Reduction}\dotfill \pageref*{evaluation_and_reduction} \linebreak
\noindent\hyperlink{variants}{Variants}\dotfill \pageref*{variants} \linebreak
\noindent\hyperlink{pure_lambda_calculus}{Pure lambda calculus}\dotfill \pageref*{pure_lambda_calculus} \linebreak
\noindent\hyperlink{simply_typed_lambda_calculus}{Simply typed lambda calculus}\dotfill \pageref*{simply_typed_lambda_calculus} \linebreak
\noindent\hyperlink{functional_programming}{Functional programming}\dotfill \pageref*{functional_programming} \linebreak
\noindent\hyperlink{related_entries}{Related entries}\dotfill \pageref*{related_entries} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

The \textbf{lambda calculus} is:

\begin{itemize}%
\item a simple [[programming language]];


\item a \emph{model of computation} (akin to [[Turing machine]]s and [[recursive function]]s), through which we can study the computability and complexity of [[functions]] and predicates; and


\item an [[internal language]] for [[cartesian closed categories]] (for more on this see at \emph{[[relation between type theory and category theory]]}).



\end{itemize}
It comes in both \emph{typed} and \emph{untyped} versions.

\hypertarget{concepts}{}\subsection*{{Concepts}}\label{concepts}

\hypertarget{abstraction_and_application}{}\subsubsection*{{Abstraction and application}}\label{abstraction_and_application}

The basic constructs of lambda calculus are \emph{[[lambda abstractions]]} and \emph{applications}. If $t$ is an expression of some sort involving a free variable $x$ (possibly vacuously), then the lambda abstraction

\begin{displaymath}
\lambda x. t
\end{displaymath}
is intended to represent the function which takes one input and returns the result of substituting that input for $x$ in $t$. Thus, for instance, $(\lambda x. (x+1))$ is the function which adds one to its argument. Lambda expressions are often convenient, even outside lambda calculus proper, for referring to a function without giving it a name.

Application is how we ``undo'' abstraction, by applying a function to an argument. The application of the function $f$ to the argument $t$ is generally denoted simply by $f t$. Applications can be parenthesized, so for instance $f(t)$ and $(f)t$ and $(f t)$ all denote the same thing as $f t$.

Application is generally considered to associate to the left. Thus $u v w$ denotes the application of $u$ to $v$, followed by application of the result (assumed to again be a function) to $w$. This allows the representation of functions of multiple variables in terms of functions of one variable via ``currying'' (named for Haskell Curry, although it was invented by Moses Sch\"o{}nfinkel): after being applied to the first argument, we return a function which, applied to the next argument, returns a function which, when applied to the next argument, \ldots{} , returns a value. For instance, the ``addition'' function of two variables can be denoted $(\lambda x. (\lambda y. x+y))$: when applied to an argument $x$, it returns a function which, when applied to an argument $y$, returns $x+y$. This is so common that it is generally abbreviated $(\lambda x y. x+y)$.

\hypertarget{evaluation_and_reduction}{}\subsubsection*{{Evaluation and Reduction}}\label{evaluation_and_reduction}

\emph{Evaluation} or \emph{reduction} is the process of ``computing'' the ``value'' of a lambda term. The most basic operation is called \emph{[[beta reduction]]} and consists in taking a lambda abstraction at its word about what it is supposed to do when applied to an input. For instance, the application $(\lambda x. x+1) 3$ reduces to $3+1$ (and thereby, presuming appropriate rules for $+$, to $4$). In general, the beta reduction of a term $(\lambda x.t)(u)$ is defined as the [[substitution\#avoiding variable capture|capture-avoiding substitution]] of $u$ for $x$ in $t$,

\begin{displaymath}
(\lambda x.t)(u) \to_\beta t[u/x].
\end{displaymath}
Terms which can be connected by a [[zigzag]] of beta reductions (in either direction) are said to be \emph{beta-equivalent}.

Another basic operation often assumed in the lambda calculus is \emph{[[eta reduction]]/expansion}, which consists of identifying a function, $f$ with the lambda abstraction $(\lambda x. f x)$ which does nothing other than apply $f$ to its argument. (It is called ``reduction'' or ``expansion'' depending on which ``direction'' it goes in, from $(\lambda x. f x)$ to $f$ or vice versa.)

A more basic operation than either of these, which is often not even mentioned at all, is \emph{alpha equivalence}; this consists of the renaming of bound variables, e.g. $(\lambda x. f x) \to (\lambda y. f y)$.

More complicated systems that build on the lambda calculus, such as various [[type theories]], will often have other rules of evaluation as well.

In good situations, lambda calculus reduction is \emph{[[confluent category|confluent]]} (the [[Church-Rosser theorem]]), so that every term has at most one \emph{[[normal form]]}, and two terms are equivalent precisely when they have the same normal form. A term is said to be \emph{normalizing} if its reduction is also terminating---more precisely, $t$ is said to be \emph{weakly-normalizing} if there exists a finite sequence of reductions

\begin{displaymath}
t \to t_1 \to t_2 \to \dots \to t_n \nrightarrow
\end{displaymath}
terminating in a normal form $t_n$, and \emph{strongly-normalizing} if \emph{all} sequences of reductions lead to a (by confluence, necessarily unique) normal form. In general, there exist terms which do not normalize by any reduction sequence, although simply-typed lambda calculus and many other typed variants of lambda calculus are strongly-normalizing.

\hypertarget{variants}{}\subsection*{{Variants}}\label{variants}

\hypertarget{pure_lambda_calculus}{}\subsubsection*{{Pure lambda calculus}}\label{pure_lambda_calculus}

In the untyped (or ``pure'') lambda calculus, every term can be applied to any other term. As an example of the sort of freedom this allows, we can form the term $u = \lambda x. x x$ which applies its argument to itself, and then define

\begin{displaymath}
\omega = u(u)
\end{displaymath}
as the self-application of $u$. Performing beta-reduction on $\omega$ yields

\begin{displaymath}
\omega \to_\beta x x[u/x] = u(u) = \omega \to_\beta \omega \to_\beta \dots
\end{displaymath}
thus giving the classic example of a non-terminating program.

In pure untyped lambda calculus, we can define [[natural numbers]] using the [[Church numerals]]: the number $n$ is represented by the operation of $n$-fold iteration. Thus for instance we have $2 = \lambda f. (\lambda x.f (f x))$, the function which takes a function $f$ as input and returns a function that applies $f$ twice. Similarly $1 = \lambda f. (\lambda x.f x)$ is the identity on functions, while $0 = \lambda f. (\lambda x . x)$ takes any function $f$ to the identity function (the 0th iterate of $f$). We can then construct (very inefficiently) all of arithmetic, and prove that the arithmetic functions expressible by lambda terms are exactly the same as those computable by Turing machines or (total) recursive functions.

The most natural sort of \emph{model} of pure lambda calculus is a [[reflexive object]] in a cartesian closed category, that is, an object $U$ together with a pair of maps

\begin{displaymath}
\itexarray{U & \overset{a}{\underset{\ell}{\rightleftarrows}} & U^U}
\end{displaymath}
representing $a$pplication and $\ell$ambda, such that $a \circ \ell = 1$ (to validate the $\beta$ equation). Such data thereby witnesses the [[exponential object]] $U^U$ as a [[retract]] of $U$. Of course there are no nontrivial such models in sets, but they do exist in other categories, such as [[domain]]s. It is worth remarking that a necessary condition on such $U$ is that every term $f \colon U^U$ have a fixed-point; see [[fixed-point combinator]].

From the point of view of [[type theory]] and in particular the ``types \`a{} la Church'' perspective, such a reflexive object $U$ can also be seen as the intrinsic type of \emph{every} lambda term, and so the untyped lambda calculus is sometimes referred to (a bit cheekily) as really being ``uni-typed''. On the other hand, from the ``types \`a{} la Curry'' perspective, it is also possible to begin with the pure lambda calculus as a foundation, and then try to ascribe individual terms more precise types. For example, the normalizing terms of pure lambda calculus can be characterized precisely as those which are typable in an [[intersection type]] system.

\hypertarget{simply_typed_lambda_calculus}{}\subsubsection*{{Simply typed lambda calculus}}\label{simply_typed_lambda_calculus}

In simply typed lambda calculus, each variable and term has a [[type theory|type]], and we can only form the application $f t$ if $t$ is of some type $A$ while $f$ is of a function type $A \to B = B^A$ whose domain is $A$; the type of $f t$ is then $B$. Similarly, if $x$ is a variable of type $A$ and $t$ is a term of type $B$ involving $x$, then $\lambda x. t$ has type $A\to B$.

Without some further type and term constructors, there is not much that can be done, but if we add a [[natural numbers object]] (that is, a type $N$ with constants $0$ of type $N$ and $s$ of type $N\to N$, along with a ``definition-by-recursion'' operator), then we can express many recursive functions. (We cannot by this means express \emph{all} computable functions, although we can go beyond [[primitive recursive function]]s; for instance we can define the [[Ackermann function]]. One way to increase the expressiveness to all [[partial recursive function]]s is to add a [[fixpoint]] [[combinator]], or an unbounded search operator).

Simply typed lambda calculus is the natural [[internal language]] of [[cartesian closed categories]]. This means that

\begin{itemize}%
\item Every cartesian closed category gives rise to a simply typed lambda calculus whose basic types are its objects, and whose basic terms are its morphisms, while


\item Every simply typed lambda calculus ``generates'' a cartesian closed category whose objects are its types and whose morphisms are its equivalence classes of terms.



\end{itemize}
These two operations are adjoint in an appropriate sense.

\hypertarget{functional_programming}{}\subsubsection*{{Functional programming}}\label{functional_programming}

Most [[functional programming|functional]] [[programming language|programming languages]], such as Lisp, ML, and Haskell, are at least loosely based on lambda calculus.

\hypertarget{related_entries}{}\subsection*{{Related entries}}\label{related_entries}

\begin{itemize}%
\item [[combinator]], [[combinatory logic]]

\begin{itemize}%
\item [[fixed-point combinator]]

\end{itemize}

\item [[type theory]]


\item [[relation between type theory and category theory]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

The idea that untyped lambda calculus can be modeled internally to a cartesian closed category as a [[reflexive object]] (an object $U$ such that the exponential $U^U$ is a [[retract]] of $U$) was formulated explicitly by [[Dana Scott]] in

\begin{itemize}%
\item Dana Scott. Relating theories of the $\lambda$-calculus. In \emph{To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism} (eds. Hindley and Seldin), Academic Press, 403--450, 1980.

\end{itemize}
This followed his earlier work constructing an explicit such model in the category of domains:

\begin{itemize}%
\item Dana Scott. Outline of a Mathematical Theory of Computation. \emph{Proc. 4th Princeton Conf. on Information Sciences and Systems}, 169--176, 1970. \href{http://ropas.snu.ac.kr/~kwang/520/readings/sco70.pdf}{pdf}


\item Dana Scott. Data types as lattices. \emph{SIAM Journal of Computing}, 5(3):522--587, September 1976.



\end{itemize}
Another, more recent take on pure lambda calculus as a certain kind of [[algebraic theory]] (called a ``[[lambda theory]]'') can be found in

\begin{itemize}%
\item [[Martin Hyland]]. Classical lambda calculus in modern dress. To appear in \emph{Mathematical Structures in Computer Science}, 2013. \href{http://arxiv.org/abs/1211.5762}{arxiv}

\end{itemize}
[[!redirects lambda calculus]] [[!redirects lambda calculi]] [[!redirects lambda-calculus]] [[!redirects lambda-calculi]] [[!redirects ∞-calculus]] [[!redirects ∞-calculi]]

[[!redirects pure lambda calculus]] [[!redirects pure lambda-calculus]] [[!redirects pure ∞-calculus]]

[[!redirects untyped lambda calculus]] [[!redirects untyped lambda-calculus]] [[!redirects untyped ∞-calculus]]

[[!redirects unityped lambda calculus]] [[!redirects unityped lambda-calculus]] [[!redirects unityped ∞-calculus]]

[[!redirects typed lambda calculus]] [[!redirects typed lambda-calculus]] [[!redirects typed ∞-calculus]]

[[!redirects simply typed lambda calculus]] [[!redirects simply typed lambda-calculus]] [[!redirects simply typed ∞-calculus]]

[[!redirects simply-typed lambda calculus]]



\end{document}