|
CMU-CS-02-150
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMU-CS-02-150
Iktara in ConCert: Realizing a Certified Grid
Computing Framework from a Programmer's Perspective
Bor-Yuh Evan Chang
June 2002
Senior Thesis
CMU-CS-02-150.ps
CMU-CS-02-150.pdf
Keywords: Grid computing, grid programming, theorem proving,
intuitionistic linear logic, ConCert
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 (Iktar), that provides motivation for and guides the design of such
a programming model.
|