Arthur Neal Glew
105 Catherine Street
Ithaca, N.Y. 14850-4654
U.S.A.
+1-607-256 8641
glew@cs.cornell.edu
http://www.cs.cornell.edu/glew
Department of Computer Science
Cornell University
c/- 4130 Upson Hall
Ithaca, N.Y. 14853-7501
U.S.A.
+1-607-255 9834
(fax) +1-607-255 4428

I was born in Wellington, New Zealand in 1972, and am a citizen of New Zealand.

Research

Interests

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, and secure extensible systems.

Experience

At Cornell I have been 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.

Third, I am currently working on additional type constructors for TAL that would 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.

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 am currently adding support for objects.  I am currently also working on a compiler for a small object oriented language to demonstrate the feasibility of my ideas for object and class encoding.

Academic

Degrees

Honours

Journal Articles

Conference Papers

Technical Reports

Talks

Employment

References


Last updated 10 Oct 2005.