Gopalan NadathurDepartment of Computer Science and EngineeringInstitute of Technology University of Minnesota 4-192 EE/CS Building 200 Union Street SE Minneapolis, MN 55455
|
|
One outcome of my research has been the development of the
higher-order logic programming language called λProlog.
This language was the first one to offer systematic support for
higher-order abstract syntax, a new way for viewing
the syntactic structure of objects such as programs, formulas, proofs
and types that occur in many symbol processing tasks.
This facet of λProlog has been exploited by many researchers
in prototyping and implementing (interactive) theorem
provers, type checkers, compilers, program transformers and generic
derivation systems. Motivated by such applications, I have led a
research project aimed at developing good ways to implement the many new
features of this language. This work is embodied in the Teyjus system that is a
compiler based realization of λProlog. Teyjus has
been used in implementing systems such as LambdaCLAM.
The λProlog language provides a framework for realizing systems
that are described by a collection of inference rules based on the
syntax of objects. I have now become interested in mechanizing
the meta-theory of such systems. A natural way to realize this
capability is by developing a facility for reasoning about
λProlog programs. The SLIMMER project that is jointly
funded by NSF and INRIA has initiated work in this
direction. In a collaboration with our colleagues from France, we have
recently combined some of our ideas relating to reasoning and
implementation to build the first version of a system that provides
such support. This system has very limited capabilities but is still
interesting: it can, for instance, be used in checking simple forms of
bisimilarity equivalence. Ongoing research seeks to develop new logical
ideas and implementation technology that will enable such a system to
support much more sophisticated reasoning tasks.
My work also spans theoretical ideas that are useful relative to
programming languages and logical frameworks. In the past, I have
developed proof theoretic ideas that have been used, for instance, in
the Twelf system, an explicit substitution notation for the
lambda calculus that has been used in the Standard ML of New
Jersey compiler and an algorithm for higher-order pattern
unification that has been implemented in four different (programming)
languages and used in at least two existing systems.
Send mail to me if you would like to join this group.
Research Interests
I am interested in the design, application and implementation of
programming languages, especially of the declarative
variety. I am also interested in logic, especially as it underlies
our understanding of computation and the structure of programming
formalisms and as it informs our construction of general reasoning
systems.
Research Opportunities for Graduate Students
If you are a UMN student interested in research in Programming
Languages and you like the challenge of thinking of theoretical issues
and the thrill of testing out your thinking by building systems, I
would like to hear from you. To actually
participate in the research, you will, of course, need to have an
adequate background and inclination. For this, you should, at a
minimum, have taken, enjoyed and done well in the Programming
Languages and the Compilers courses that we offer at UMN.
Research Opportunities for Undergraduates
If you are an undergraduate in the junior or senior year and are
genuinely interested in a hands-on experience in programming languages
research, I may have some projects that interest you. To participate
constructively in this work and also to really enjoy it, there are
some prerequisites: You should have taken a course like CSci 5106 at
UMN that has exposed you to programming language principles, you
should know something about, and be interested in, system building and
you should like mathematics and mathematical reasoning. Come talk to
me if you have all these attributes or even if you think you do but
have still to find out for sure.
Programming Languages Seminar
A group of interested students and faculty members meet for about an
hour and a half each week to discuss a research paper or two that we
have collectively decided to read a couple of weeks before. The
meeting time for Spring 2006 is 3:30 - 5:00 p.m. on Fridays. The cost
of participation is small: you mainly have to agree to lead the
discussion of a paper every now and then. The benefits of
participation are substantial: you learn about some of the research
trends in the programming languages area, you get to hone your skills
for reading such papers in a friendly and encouraging setting, you get
to interact with a group of nice people and you partake of the goodies
someone brings each week to the meeting.
Professional Activities
Editorial and Related Duties
Conference Program Committees
Currently Planned Travel
No planned travel yet for Spring 2006.
Current and Recent Courses