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.


Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu