| Research | |
|
My broad area of interest in Computer Science is Programming
Languages. Specifically, I am interested in semantics of typed
functional languages, type theory, logic and its relation to types,
and proof theory and automated synthesis of efficient proofs. I'm
also interested in the application of formal methods to safety and
security issues in practical settings.
For my Ph.D. thesis, I worked on the foundational proof-carrying code
project at Princeton under Prof. Andrew Appel, details of which can be
found at http://www.cs.princeton.edu/sip/projects/pcc/. The main aim of
this project is to build the infrastructure to produce programs that are
provably safe. As a part of this project, my research focussed on
building a low level type system with a powerful set of primitives which
would allow a variety of high-level languages like Java or ML to be
compiled down to. The soundness of the type system is a formally
proved theorem, which helps guarantees safety of type checked programs.
I am currently working as a postdoctoral research associate at Rice
University. My projects here involve the use of multi-stage programming
to automatically generate code that is provably safe without affecting
the runtime efficiency. A long term goal of this project is to be able
to apply the multi-stage technology to generate safe device drivers.
|
| Education |
|
|
- 2003 Princeton University, Ph.D.
- 1999 Princeton University, M.A., Computer Science, GPA 4.0
- 1996 Pune University, India, M.Sc., Computer Science
|
| Employment History |
|
|
|
| Rice University
|
Postdoctoral Research Associate |
| Houston, TX |
2003 - |
|
Working on projects that involve generation of provably safe
and efficient programs using multi-stage programming technology.
|
|
| Princeton University
|
Teaching Assistant |
| Princeton, NJ |
|
|
Fall 02
|
Teaching Assistant for COS217 : Introduction to
Programming Systems. Conducted weekly precepts, helped
design exams, and graded assignments.
|
|
Fall 01
|
Teaching Assistant for COS302 : Introduction to Artificial
Intelligence. Helped design assignments and graded them.
|
|
Fall 98
|
Teaching Assistant for COS302 : Introduction to Artificial
Intelligence. Graded assignments.
|
|
Spring 98
|
Teaching Assistant for COS333 : Advances Programming Techniques.
Graded assignments.
|
|
Fall 97
|
Teaching Assistant for COS217 : Introduction to Programming
Systems. Conducted weekly precepts, graded assignments.
|
|
|
| Intel Corporation
|
Research Intern |
| Santa Clara, CA |
Summer 2002 |
|
Intern in the Programming Systems Laboratory at MRL, Intel, Santa Clara. Helped refine type system
for the internal representation of a just-in-time compiler, StarJIT, so that its safety could be
ensured.
|
|
| Princeton University
|
Research Assistant |
| Princeton, NJ |
Spring 1999 |
|
Worked on the Zephyr component of the National Compiler
Infrastructure project and developed an expander for the
i386 architecture.
|
|
| Tata Research Development And Design Center
|
Project Engineer |
| Pune, India |
May 1996 - July 1997 |
|
Project Engineer in the Language Processing division. Involved in design and implementation
of various tools for language processing.
|
|
| Computer Science Dept., Pune University
|
Course Lecturer |
| Pune, India |
Aug 1996 - Dec 1997 |
|
Lectured for a course on Programming Language Semantics at Department of Computer Science,
University of Pune, India. Helped design and grade assignments and exams.
|
|
|
| Awards and Honours |
|
|
- Ranked 1st in University of Pune for M.Sc. ( Computer Science ) degree course.
- Ranked 2nd in University of Pune for Bachelor of Computer Science degree course.
|
| Papers |
|
|
-
Efficient Substitution in Hoare Logic Expressions,
with Andrew Appel and Roberto Virga, In 4th International
Workshop on Higher-Order Operational Techniques in Semantics,
Sep 2000.
-
Foundational Semantics for TAL Syntactic Rules via Typed
Machine Language, with Andrew Appel,
Princeton University, Mar 2002.
-
A Kind System for Typed Machine Language,
with Christopher Richards and Andrew Appel,
Princeton University, Sep 2002.
- Construction of a Semantic Model for a Typed Assembly Language,
with Gang Tan, Dinghao Wu, and Andrew Appel, In Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04), Venice, Italy, Jan 2004
|
| Programming Skills |
|
|
I have worked on projects in ML, Lisp, Prolog, Twelf, C, C++, Java, and
Perl in the UNIX environment.
|
| References |
|
|
- Andrew Appel, Professor,
Computer Science Department,
Princeton University,
Princeton, NJ 08544.
appel(AT)cs.princeton.edu
- Amy Felty, Associate Professor,
School of Information Technology and Engineering,
University of Ottawa,
800 King Edward Ave.,
Ottawa, Ontario, Canada KIN 6N7.
afelty(AT)site.uottawa.ca
- Dr. Ali-Reza Adl-Tabatabai, Research Scientist,
Microcomputer Research Labs,
2200 Mission College Blvd.,
Santa Clara, CA 95052-8119
ali-reza.adl-tabatabai(AT)intel.com
|
| Citizenship |
|
|
I am an Indian citizen on an F1 student visa.
|