Difference between revisions of "TACL Seminar Spring '04"

From CSWiki
Jump to: navigation, search
m (Spring '04 Schedule)
m (Spring '04 Schedule)
Line 9: Line 9:
 
|-
 
|-
 
| Feb 27 || align="center" colspan="3" | [http://www.cis.upenn.edu/~stevez/njpls/feb04.html New Jersey Programming Languages and Systems Day (NJPLS)]
 
| Feb 27 || align="center" colspan="3" | [http://www.cis.upenn.edu/~stevez/njpls/feb04.html New Jersey Programming Languages and Systems Day (NJPLS)]
 +
|-
 +
| Mar 24 || [http://www.cs.princeton.edu/~ljia/ Limin Jia] || Modal Proofs as Distributed Programs || [[TACL_Seminar_Spring_'04#Limin_Jia | Abstract]] / [http://www.cs.princeton.edu/~ljia/research/papers/esop04.pdf Paper]
 
|-
 
|-
 
| Apr 16 || [http://www.cs.cmu.edu/~crary/ Karl Crary (CMU)] || Grid Computing and Foundational Certified Code || [[TACL_Seminar_Spring_'04#Karl_Crary | Abstract]]
 
| Apr 16 || [http://www.cs.cmu.edu/~crary/ Karl Crary (CMU)] || Grid Computing and Foundational Certified Code || [[TACL_Seminar_Spring_'04#Karl_Crary | Abstract]]

Revision as of 18:00, 27 August 2006

TACL Seminar

Spring '04 Schedule

Date Speaker Title Links
Feb 26 Aaron Stump (WUSTL) Static Validation of a Type-Preserving Compiler Abstract
Feb 27 New Jersey Programming Languages and Systems Day (NJPLS)
Mar 24 Limin Jia Modal Proofs as Distributed Programs Abstract / Paper
Apr 16 Karl Crary (CMU) Grid Computing and Foundational Certified Code Abstract
May 21 IBM Research Programming Languages Day

Abstracts

Aaron Stump

Static Validation of a Type-Preserving Compiler

In their paper 'From System F to Typed Assembly Language', Morrisett, Walker, Crary, and Glew give a formal definition of a multi-stage compiler from a polymorphic functional programming language down to a (typed) assembly language. Each compiler stage is shown to be type-preserving: well-typed input programs are translated to well-typed output programs. This result is established for the mathematical description of the compiler stages, not an actual implementation of the compiler.

This talk describes work in progress to validate statically the following property of an actual implementation of the compiler: in the absence of certain run-time errors, any output program produced by a compiler stage for a typable input program is guaranteed to type check. This is achieved by writing the compiler in a proposed new language called Rogue-Sigma-Pi (RSP), which extends the Edinburgh Logical Framework (LF) with constructs for imperative programming with explicit recursion. A compiler stage is then written as a translation from proofs of typing judgments in the source language to proofs of typing judgments in the target language. RSP's type system can validate that proofs are manipulated in a sound way.

Karl Crary

Grid Computing and Foundational Certified Code

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.)


TACL Seminar