Neal Glew's Resume

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.

Research

Interests

Experience

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.

Academic

Degrees

• PhD in Computer Science, Cornell University, Jan 2000.
• MS in Computer Science, Cornell University, Dec 1997.
• BSc(Hons) First class in Computer Science, Victoria University of Wellington, completed Nov 1993, conferred June 1994.
• BSc in Mathematics and Computer Science, Victoria University of Wellington, completed Nov 1992, conferred June 1994.

Honours

• Sir Robert Stout Scholarship

  "awarded to the student who shall be adjudged by the Academic Board to be the best student who has completed all examination requirements for a first Bachelor's degree in the previous academic year"
  

Journal Articles

• Michal Cierniak, Marsha Eng, Neal Glew, Brian Lewis, and James Stichnoth. The Open Runtime Platform: a flexible high-performance managed runtime environment. In Concurrency and Computation: Practice and Experience, Special Issue on Java Grande 2002, in publication.
• Todd Anderson, Marsha Eng, Neal Glew, Brian Lewis, Vijay Menon, and James Stichnoth. Experience Integrating a New Compiler and a New Garbage Collector Into Rotor. In Journal of Object Technology, special issue on .NET Technologies 2004, 3(9), 2004.
• Neal Glew and Jens Palsberg.  Type-safe method inlining.  In Science of Computer Programming, 52(2004):281-306, June 2004.
• Greg Morrisett, Karl Crary, Neal Glew, and David Walker.  Stack-Based Typed Assembly Language.  In Journal of Functional Programming, 12(1):43-88, January 2002.
• Greg Morrisett, David Walker, Karl Crary, and Neal Glew.  From System F to Typed Assembly Language.  In ACM Transactions on Programming Languages and Systems, 21(3):428-569, May 1999.

Conference Papers

• Neal Glew and Jens Palsberg. Method Inlining, Dynamic Class Loading, and Type Soundness. In Formal Techniques for Java-like Programs, Oslo, Norway, June, 2004.
• Todd Anderson, Marsha Eng, Neal Glew, Brian Lewis, Vijay Menon, and James Stichnoth. Experience Integrating a New Compiler and a New Garbage Collector Into Rotor. In .NET Technologies'2004, Plzen, Czech Republic, June 2004.
• Neal Glew, Spyros Triantafyllis, Michal Cierniak, Marsha Eng, Brian Lewis, and James Stichnoth. LIL: An Architecture-Neutral Lanugage for Virtual-Machine Stubs. In 3rd Virtual Machine Research and Technology Symposium, San Jose, CA, USA, May 2004.
• Michal Cierniak, Neal Glew, Spyros Triantafyllis, Marsha Eng, Brian Lewis, and James Stichnoth. Object-Model Independence via Code Implants. In Multiparadigm Programming with Object-Oriented Languages, Anahiem, CA, USA, October 2003.
• Michal Cierniak, Marsha Eng, Neal Glew, Brian Lewis, and James Stichnoth. Resource Use in the Interaction of Managed and Unmanaged Code. In Mobile Object Systems 2003, Resouce-Aware Computing, Darmstadt, Germany, July, 2003.
• Neal Glew and Jens Palsberg. Type-Safe Method Inlining. In The European Conference on Object-Oriented Programming 2002, Malaga, Spain, pages 525-544 of LNCS 2374, Springer, June 2002.
• Martín Abadi, Neal Glew, Bill Horne, and Benny Pinkas. Certified Email with a Light On-line Trusted Third Party: Design and Implementation. In The Eleventh World Wide Web Conference, Honolulu, HI, USA, May 2002.
• Neal Glew. A Theory of Second-Order Trees. In the European Symposium on Programming 2002, Grenoble, France, pages 147-161 of LNCS 2305, Springer, April 2002.
• Neal Glew. An Efficient Object and Class Encoding. In Conference on Object-Oriented Programming, Languages, Systems, and Applications, pages 311-314, Minneapolis, MN, USA, Oct 2000.
• Neal Glew.  Object Closure Conversion.  In 3rd International Workshop on Higher Order Operational Techniques in Semantics, Paris France, September 1999.
• Neal Glew.  Type Dispatch for Named Hierarchical Types.  In 4th International Conference on Functional Programming, pages 172-182, Paris France, September 1999.
• Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic.  TALx86: A Realistic Typed Assembly Language.  In ACM SIGPLAN Workshop on Compiler Support for System Software, Atlanta, GA, USA, INRIA Research Report 0228, pages 22-25, May 1999.
• Neal Glew and Greg Morrisett.  Type-Safe Linking and Modular Assembly Language.  In 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 250-261, San Antonio, TX, USA, January 1999.
• Greg Morrisett, Karl Crary, Neal Glew, and David Walker.  Stack-Based Typed Assembly Language.  In 2nd International Workshop on Types in Compilation, Kyoto, Japan, March 1998.  Lecture Notes in Computer Science, vol. 1473, pages 28-52.   Springer-Verlag, Berlin Germany.
• Greg Morrisett, David Walker, Karl Crary, and Neal Glew.  From System F to Typed Assembly Language.  In 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 85-97, San Diego, CA, USA, January 1998.