Paul, You never sent an April Fool joke this year. I hope every thing is fine! I thought of you on 4/1. I was also hoping to see you at the last WG2.8 meeting. WIll you be attending the FPCA this year? Are you guys hiring this year? Shail Adiya (have you met him?) has applied for a job at Yale. If you want a programming languages person - he is worth considering. I think he is truly outstanding. My letter for him is attached at the end of this note. cheers, Arvind --------------------- A letter of reference for Mr. Shail Aditya - ----------------------------------------- It is a pleasure for me to write a letter for Shail Aditya who is among the very best students that I have supervised over the years. This group of students includes Prof. Keshav Pingali at Cornell, Prof. David Culler at Berkeley and Prof. Greg Papadopoulos at M.I.T. (currently on leave at SUN). Shail came to M.I.T. in 1987 from I.I.T., New Delhi, where he had graduated first in his class. Since no two outstanding students are the same - in the following letter I will describe Shail's major contributions and characteristics. Shail's most important and impressive contribution to date is in Part 1 of his Ph.D. thesis. The problem he has solved may be described as follows: In polymorphic functional languages, many operations such as "map" (on a list) are implemented imperatively for the sake of efficiency. Functional languages, such as SML or Id, which have been extended with imperative data structures allow the programmer to express these efficient implementations as user programs in the extended language. However, imperative data structures and functional data structures have different types and thus, all the functions that operate on them have different types. As a consequence, the worlds of functional and imperative data structures remain separated for the user. Is it possible to "convert" or "coerce" a imperative data structure into a functional one in a "safe" manner? Is it possible to create a data structure using the most efficient imperative operations and then "close" it, that is, turn it into a "read-only" or a purely functional data structure? Shail has taken a Hindley-Milner style type system extended with imperative types (i.e., Leroy's Closure type system) and introduced such a "close" operation. He has proven that his close operation is safe in the sense that an object that has been closed successfully cannot be modified by any other part of the program. The system works in the presence of higher-order functions and with almost the same degree of polymorphism as if the object was created in a functional manner. Shail's solution is simpler than Gifford's effect based type systems and its modern refinements. My excitement for Shail's work stems from several different aspects of it. Firstly, Shail's system has solved an outstanding technical problem after several futile attempts. In Id (the language used in my group) all functional data structures are de-sugared into I-Structures, a fairly benign type of imperative data structure. For years the compiler has treated, for example, list and array function libraries in a special manner to restore their full functional type. With the close operation these libraries will become genuine user code. Secondly, the proof of the safety of the close operation is given with respect to the dynamic semantics of the language. Such proof are uncommon because they tend to be very difficult. Shail has provided an elegant proof of the soundness of the close operation in his thesis. However, my greatest excitement for this work stems from the fact that I expect it to be of great use in any typed imperative language (even C, with some restrictions on "malloc" etc. to make it type safe). The programmer could close a data structure after creating it and after that the other parts of the program will only be able to "read" it. The type system will determine if the close operation was used safely or not. Such a system may be of use, for example, in generating parallel code, inter-language operability etc. Furthermore, the type system may be considerably simpler for languages which do not allow passing function values up words. Shail proposes to pursue the practical implications of his system for the C language in the near future. Part 2 of Shail's thesis deals with the problem of type reconstruction which he had solved two years ago. The problem is, "Can the exact type of each object in a polymorphic language be reconstructed from the compile-time type information and the call tree if the program execution is stopped in the middle?'' This question is of practical interest for debugging, and garbage collection, among other things. The answer to this question turns out to be negative because there are cases of unrecoverable loss of type information. However, if one saves some type information at the time of certain procedure calls, then the type can be reconstructed. Shail has come up with a practical solution to the problem and has done an excellent job of implementing it in the Id compiler and its associated Run Time System. He and Alex Caro published a paper on type reconstruction and its use in the Monsoon debugger in FPCA 93. He along with Jamey Hicks and Christine Flood published a paper on garbage collection based on types LFP 94. Both these papers were written primarily by him and for the latter he also did a lot of system-level implementation work. Part 2 of his thesis also contains a proof of correctness of his type reconstruction scheme. There is more technical depth in this work than what one might imagine at first thought. Shail's very first task in my group was to implement the type-checking module in the Id compiler. The innovative aspect of the work was the incremental type checking scheme that he and Nikhil devised for Hindley-Milner style polymorphic languages. It allows separate compilation and dynamic linking of programs written in such languages. This work led to his master's thesis under the supervision of Professor Nikhil and was published in FPCA 91. Recently Shail, Joe Stoy and I have finished a paper on the semantics of a barrier construct for non-strict multi-threaded parallel languages. Again as always it was a pleasure to work with a person like Shail. He runs with ideas; he dissects them and reveals weaknesses that nobody knew existed; he polishes them until their robustness is obvious. It is due to these qualities that he had naturally assumed the leadership role in the project to write the Id compiler in Id several years ago (this was also the time when he was unable to solve the "close" problem). Shail has a superb analytical mind and all the traits of a brilliant student. He surprised me by doing exceedingly well in hardware oriented VLSI courses. Professor Anant Agarwal, his instructor in the VLSI course, told me once that Shail was the best student in his class! Shail gives excellent lectures and writes well. His publication record is very good, especially because he is the primary author on all the papers he has published to date. Shail has a wonderful personality. He is extremely cooperative and has helped many undergraduates and graduates with their projects. He has already matured as a researcher and has been setting his own research agenda. In the last two years, Shail has clearly emerged as a leader among my graduate students. Shail is as good a theoretician as Pingali was at this stage in his career and better than Zena Ariola, another recent graduate from my group who is now a professor at University of Oregon. His programming skills are considerable though a notch below Ken Traub (Exa Corp.) and Jamey Hicks (Motorola), some of the best hackers to have graduated from my group. As compared to David Culler or Greg Papadopoulos at the same stage in their careers, he is less self assured in leading a group of students totally by himself. (Maybe programming languages and compiler people are less flamboyant than their counterparts in architecture)! However, this is likely to change very rapidly as he goes out of MIT. Taking everything into account, Shail Aditya should be among the best students (if not the best student) to be graduating this year in programming languages and compilers. It will be a pleasure to have him as a colleague on the MIT faculty. I recommend him most highly to you for a research position. Sincerely, Arvind Charles W. and Jennifer C. Johnson Professor of Computer Science and Engineering