  Session types are a type discipline for communication channel endpoints which
allow conformance to protocols to be checked statically. Safely implementing
session types requires linearity, usually in the form of a linear type system.
Unfortunately, linear typing is difficult to integrate with graphical user
interfaces (GUIs), and to date most programs using session types are command
line applications.
  In this paper, we propose the first principled integration of session typing
and GUI development by building upon the Model-View-Update (MVU) architecture,
pioneered by the Elm programming language. We introduce
$\lambda_{\textsf{MVU}}$, the first formal model of the MVU architecture, and
prove it sound. By extending $\lambda_{\textsf{MVU}}$ with \emph{commands} as
found in Elm, along with \emph{linearity} and \emph{model transitions}, we show
the first formal integration of session typing and GUI programming. We
implement our approach in the Links web programming language, and show examples
including a two-factor authentication workflow and multi-room chat server.
