Yarrow is an interactive proof assistant based on the theory
of Pure Type Systems, a family of typed lambda calculi.
It offers both graphical
and textual interfaces. It has been coded entirely in Haskell,
making use of the Fudget library for the graphical interface.
In this paper we concentrate on the software architecture of
Yarrow, in particular the coupling of user
interface and proof engine.
We also treat the presentation of proofs in the flag-style format.