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









Reply via email to