With the vast amount of computing resources distributed throughout the
world today, the prospect of effectively harnessing these resources
has captivated the imaginations of many and motivated both industry
and academia to pursue this dream.  We believe that fundamental to the
realization of this dream is the establishment of trust between
application developers and resource donors, for donors often receive
little or no direct reward for their contributions.  The ConCert
project (to which this specific undertaking contributes) seeks to
develop the theoretical and engineering foundation for grid computing
in such a trustless setting based on the notion of certified code.

In this paper, we seek to drive an initial implementation of a real
grid framework from a programmer's perspective.  Specifically, we
present a model for programming the grid and a case study of a
specific application, namely a theorem prover for intuitionistic
linear logic (Iktara), that provides motivation for and guides the
design of such a programming model.