March 17, 1999 Meeting
"Look, Ma, no metatheorems": Types for proof-carrying code
A simple and efficient natural merge-sort for lists
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.
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.
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.
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 /