View source for TACL Seminar Spring '04

[[TACL Seminar]]

==Spring '04 Schedule==
{| border="1"
|-
! Date !! Speaker !! Title !! Links
|- 
| Feb 26 || [http://www.cse.wustl.edu/~stump/ Aaron Stump (WUSTL)] || Static Validation of a Type-Preserving Compiler || [[TACL_Seminar_Spring_'04#Aaron_Stump | Abstract]]
|-
| 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]]
|- 
| May 21 || align="center" colspan="3" | [http://researchweb.watson.ibm.com/compsci/plansoft/plday/plday2004.html 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.

===Limin Jia===
'''Modal Proofs as Distributed Programs'''

We develop a new foundation for distributed programming languages by
defining an intuitionistic, modal logic and then interpreting the modal
proofs as distributed programs.  More specifically, the proof terms for
the various modalities have computational interpretations as remote
procedure calls, commands to broadcast computations to all nodes in the
network, commands to use portable code, and finally, commands to invoke
computational agents that can find their own way to safe places in the
network where they can execute.  We prove some simple meta-theoretic
results about our logic as well as a safety theorem that demonstrates that
the deductive rules act as a sound type system for a distributed
programming language.

[http://www.cs.princeton.edu/~ljia/research/papers/esop04.pdf ESOP '04 Paper]

===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]]