Neal Glew's Resume

Arthur Neal Glew 
440 N Winchester Blvd Apt 13
Santa Clara CA 95050-6328
+1-408-420 3685
+1-408-564 5458

I was born in Wellington, New Zealand in 1972, and am a citizen of New Zealand. I am current a permanent resident of the USA.



I am interested in the theory of programming languages, particularly the theory underlying language implementations, and in the applications of this theory to compilers, compiler debugging, secure extensible systems, and security in general.


At Cornell I was involved in a project to design and implement a Typed Assembly Language (TAL) and various type directed compilers that target TAL.  TAL is an assembly language augmented with typing annotations and memory management primitives.   There are typing rules that specify when a TAL program is type correct, and type correct TAL programs have certain guaranties, in particular, memory safety (the program accesses only memory it has access to), control flow safety (a program jumps to and executes only valid code), and type abstraction preservation.

These guaranties can be used, in much the same way JVML is used in web browsers, to build a secure extensible system.   Unlike JVML, a system based on TAL does not trust a JVM interpreter or JIT and extension writers can aggressively optimise their extensions off line and still produce type correct TAL code.  Also, a number of different source languages can be compiled to TAL in an efficient manner, whereas, JVML is very Java specific.  However, TAL is specific to a particular architecture and is not as portable as JVML.  TAL could also be used as the target for a type directed compiler and we have implemented two examples of such compilers for a type-safe C-like language and for a subset of Scheme.

In investigating TAL and compiling to TAL we have formalised some interesting aspects of low level code.  For example, in our TIC'98 paper, where we described adding support for stacks to TAL, we were able to formally specify calling conventions as a type translation from function types to TAL code types.  We demonstrated how to encode different calling conventions including register based and stack based passing and returning conventions, caller pop versus callee pop, and callee saves registers.

Our particular implementation, called TALx86, is based on the instruction set of IA32 (Intel's 32-bit architecture, implemented by, for example,  the Pentium Processor).   TALx86 is a scaled up version of TAL and contains support for integers, records, unions, arrays, and exceptions and provides a suitable target for the compilation of procedural and functional languages such as C, Pascal, ML, Haskell, and Scheme.

My contributions to the project have been both theoretical and practical.  On the theory side, I formalised a module system for TAL.  Source level module systems can be compiled to TAL's, and separate compilation and type checking are possible.   Furthermore, a link checker can verify that a collection of compiled modules make consistent assumptions about the namespace and types of names, and a program checker can verify that the collection constitutes a complete program, including checking the type of the program's entry label.  Both of these checkers use only interface information and do not require rechecking the instructions or data of the TAL modules.  In addition to being a module system for TAL, the formalism provides a formal theory of linking extending previous work by Cardelli.  Cardelli provided an initial formalisation of the process of linking but did not model the labels used by linker tools, cyclic references between modules, abstract types, abstract type constructors, functors, or dynamic linking.  My work extends his providing satisfactory solutions for all of the above except dynamic linking.

A second work was on type dispatch for named hierarchical types.  A number of languages allow the user to dispatch on the runtime type of a value.  For example, Scheme has predicates for testing whether a value is an integer, a pair, the empty list, et cetera, and Java has a downcasting expression for checking if an object is an instance of some class.  In typed languages, these mechanisms cause type refinement: The type of the value being dispatch on is changed to reflect the new information.   While type dispatch mechanisms have been studied for structural types in the absense of subtyping, neither named types, nor the presence of subtyping has been addressed before.  I formalised a tagging language that contains the core mechanism for named types with subtyping.  This mechanism underlies a number of constructs including class casting, class case, exceptions, hierarchical extensible sums, and multimethods.  Implementations of this tagging mechanism typically use newly created heap blocks to represent each named type and pointer equality to do the type dispatch.  I formalised an example implemenation as a translation into a typed lambda calculus, showing how to use a new type constract, tag types, to connect the pointer comparisons to type refinement of the values being dispatched upon.  These ideas are used in TALx86 to implement exceptions without an ad hoc mechanism, and eventually will be used to implement downcasting in object oriented languages.

A third work was on additional type constructors for TAL that enable an efficient implementation of object oriented languages, particularly, single-inheritance class-based languages such as Java.  The principle new construct is the self quantifier and is used to express the type of self in the translation of an object to a record of functions. I formalised a small single-inheritance class-based language and showed how to translate it into a typed lambda calculus with self quantifiers, F-bounded polymorphism, and equirecursive types. My translation used a well known and efficient technique for virtual dispatch. A key part of this work was finding the right formulation for self quantifiers, as previous work on self quantifiers had rules that are too weak for my translation. This work has also lead to the investigation of decidability of subtyping for second-order systems with F-bounded polymorphism and equirecursive types. I recently submitted the first part of this work and hope to submit the remaining part soon.

On the implementation side, I was responsible for a large part of the TAL type checker including adding subtyping, a module system, a link verifier, a program verifier, and tag types. I also did some work adding support for objects and on a compiler for a small object-oriented language to demonstrate the feasibility of my ideas for object and class encodings.




Journal Articles

Conference Papers

Technical Reports




Last updated 31 Jan 2005.