\begin{abstract}
  Formal constructive type theory has proved to be an effective
  language for mechanized proof.  By avoiding non-constructive
  principles, such as the law of the excluded middle, type theory
  admits sharper proofs and broader interpretations of results.  From
  a computer science perspective, interest in type theory arises from
  its applications to programming languages.  Standard constructive
  type theories used in mechanization admit computational
  interpretations based on meta-mathematical normalization theorems.
  These proofs are notoriously brittle; any change to the theory
  potentially invalidates its computational meaning.  As a case in
  point, Voevodsky's univalence axiom raises questions about the
  computational meaning of proofs.

  We consider the question: \emph{Can higher-dimensional type theory
    be construed as a programming language?}  We answer this question
  affirmatively by providing a direct, deterministic operational
  interpretation for a representative higher-dimensional dependent
  type theory with higher inductive types and an instance of
  univalence.  Rather than being a formal type theory defined by
  rules, it is instead a computational type theory in the sense of
  Martin-L\"{o}f's meaning explanations and of the NuPRL semantics.
  The definition of the type theory starts with programs; types are
  specifications of program behavior.  The main result is a
  canonicity theorem stating that closed programs of boolean type
  evaluate to true or false.
\end{abstract}