[Pl-seminar] Karl Crary @ Harvard, Monday, 2pm

[Greg Morrisett]

Karl Crary from Carnegie Mellon will be visiting Harvard on Monday,
and giving a talk at 2pm in Maxwell Dworkin 221.  The title and
abstract for the talk are below.  If you would like to come and
need directions, please let me know.

-Greg Morrisett

Grid Computing and Foundational Certified Code
Karl Crary, Carnegie Mellon University

Monday, June 7th  2:00 pm
Maxwell Dworkin 221

Grid computing seeks to harness idle computing power on the Internet to 
create a huge supercomputer available to the public. Many obstacles 
exist to making this vision a reality; a primary obstacle is the 
understandable reluctance of computer owners to execute code from 
sources they do not trust. This obstacle limits participation in the 
grid to the small number who can afford to cultivate pre-arranged trust
relationships for their applications.

The ConCert project seeks to make the grid universally usable by 
eliminating the need for trust when disseminating applications. This is 
achieved using certified code to ensure that grid applications comply 
with a safety policy. However, certified code can raise other obstacles 
to universal usability. In particular, if a safety policy is overly 
specific, it may unnecessarily limit the number of applications that can 
comply, and therefore limit the number that can use the grid. This talk 
discusses our work to resolve this issue through foundational certified 
code, wherein the safety policy is as general as possible. Foundational 
certified code has been infamously difficult to work with,  as its 
certificates must include complete (and typically complicated) safety 
arguments to the level of the concrete architecture that tend. We 
discuss our system, called TALT, which employs a unique methodology 
based in metalogic and operational semantics that ameliorates these 
difficulties.

(This is joint work with Susmit Sarkar)