\documentclass[a4paper,12pt]{report}

\begin{document}

\title{Report on the Programming Language Hao\thanks{DRAFT---DO NOT CITE!}}
\author{Antti-Juhani Kaijanaho}

\maketitle

\chapter{Introduction}

\chapter{The core language}

Almost all program constructs in Hao are \emph{terms}.

A term is \emph{well-formed} iff it has a type.  A term has a
\emph{denotation} if it is well-formed.

Types and terms are categorized as follows:
\begin{itemize}
\item A term whose type is a \emph{kind} is a \emph{type expression}.
  The denotation of a type expression is a \emph{type}.
\item A term whose type is a \emph{value type} is a \emph{value expression}.
  The denotation of a value expression is a \emph{value}.
\item A term whose type is a \emph{statement type} is a
  \emph{statement}.  The denotation of a statement is a
  \emph{program}.
\end{itemize}

The binding term $x = t$ binds $x$ to the denotation of $t$.  If the
name is already bound in an enclosing scope, the old binding is
shadowed.  If the name is already bound in this scope, the term is not
well-formed.  The type of $x = t$ is the type of $t$ and the
denotation of $x = t$ is $t$.  The effect of $x = t$ is the effect of
$t$.

In the sequencing term $t ; t'$, if $t$ modifies the environment, then
$t'$ assumes that modified environment.  The type and denotation of $t
; t'$ is the type and denotation, respectively, of $t'$.  The effect
of $t ; t'$ is the sequencing of the effects of $t$ and $t'$.

The operator application term $t \circ t'$ is syntactic sugar for the term
$(\circ) \; t \; t'$.

The application term $t \; t'$ is analyzed as follows:
\begin{itemize}
\item If the type of $t$ is a kind of the form $\kappa_1 \to \kappa_2$
  and the type of $t'$ is the kind $\kappa_1$, then the term $t \; t'$
  is well-formed.  The type of $t \; t'$ is $\kappa_2$.  The
  denotation of $t \; t'$ is the specialization of the type operator
  denotation of $t$ with the type denotation of $t'$.  The term $t \;
  t'$ has no effect.
\item If the type of $t$ is a kind of the form $\tau \to \kappa$ and
  the type of $t'$ is the value type $\tau$, then the term $t \; t'$
  is well-formed.  The type of $t \; t'$ is $\kappa$.  The
  denotation of $t \; t'$ is the specialization of the type operator
  denotation of $t$ with the value denotation of $t'$.  The term $t \;
  t'$ has no effect.
\item If the type of $t$ is a value type $\tau_1 \to \tau_2$ and the
  type of $t'$ is the value or statement type $tau_1$, then the term
  $t \; t'$ is well-formed.  The type of $t \; t'$ is $\tau_2$.  The
  denotation of $t \; t'$ is the application of the function
  denotation of $t$ to the denotation of $t'$. XXX
\end{itemize}

\chapter{Conclusion}

\end{document}