March 17, 1999 Meeting

10:00am Andrew Appel "Look, Ma, no metatheorems": Types for proof-carrying code

10:45am Olin Shivers A simple and efficient natural merge-sort for lists

11:15am Break

11:30am Jens Palsberg From Polyvariant Flow Information to Intersection and Union Types

How does flow analysis relate to type systems? In our POPL'98 paper we presented a way of understanding polyvariant flow information in terms of intersection and union types. Further investigation has revealed that it is also possible to understand intersection and union types in terms of polyvariant flow information. The result is an equivalence theorem which relates an inductively-defined type system and a co-inductively-defined polyvariant flow analysis. We have used this result as basis for a new flow type system in the spirit the Lambda-CIL calculus of Wells, Dimock, Muller, and Turbak. As usual, the idea is that types are annotated with flow information. Our flow type system is both simpler and more powerful than Lambda-CIL, and we are now investigating if it has advantages as a typed intermediate language. Joint work with Christina Pavlopoulou.

12:15pm Lunch

1:30pm Riccardo Pucella: SML/NJ interoperability through IDL

IDL is a standard language to describe interfaces to components, including libraries, with a syntax close to C. We show how we can automatically derive from an IDL description of a library the SML code required to interface to that library. We describe different translation modes, both low-level and high-level, and extensions to handle component-based interfaces, such as COM.

2:15pm Satish Chandra Physical Type Checking for C

In C, a pointer of a given type can be cast into any other pointer type. Because of this, a programmer can interpret any region of memory to be of any type. Traditional type checking for C (as in a C compiler) cannot enforce that such reinterpretation of memory is done in a meaningful way, because the C standard allows arbitrary type conversions between pointer types. Moreover, use of casts can make legacy code harder to understand and maintain. In this talk, I'll describe recent work I have done in applying program analysis techniques to cope with type casts in C programs.

3:00pm Break

3:15pm David Naumann Data refinement in a higher order refinement calculus

We show soundness of data refinement for an imperative language with stored procedures and specification constructs, using predicate transformer semantics. Data refinement is based on forward simulations, for which we use a simple robust categorical formulation. We compare this formulation with recent work by Plotkin, Power and Sannella on generalized logical relations.

4:00pm Talks End

Dave MacQueen / dbm@research.bell-labs.com