|   | CMU-CS-02-150 Computer Science Department
 School of Computer Science, Carnegie Mellon University
 
    
     
 CMU-CS-02-150
 
Iktara in ConCert: Realizing a Certified GridComputing Framework from a Programmer's Perspective
 
Bor-Yuh Evan Chang 
June 2002  
Senior Thesis  
CMU-CS-02-150.psCMU-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.
 
 |