Yarrow is an interactive proof assistant based on the theory
of Pure Type Systems, a family of typed lambda calculi. Yarrow
has been designed as a flexible environment for experimentation 
with various 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 use of monads, the coupling of user
interface and proof engine, polymorphic output routines,
and flexible representations of lambda terms.
We also treat the presentation of proofs in the flag-style format.