[PRL] reminder

[Matthias Felleisen]

I strongly recommend that you attend this talk, if you can spare the 
time. -- Matthias


Begin forwarded message:

> From: Greg Morrisett <greg at eecs.harvard.edu>
> Date: June 3, 2004 3:18:22 PM EDT
> To: church-active at types.bu.edu, pl-seminar at lists.ccs.neu.edu, 
> programming at eecs.harvard.edu
> Cc: Subject: [Pl-seminar] Karl Crary @ Harvard, Monday, 2pm
>
> 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)
>
>
>
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar