|
I have developed a higher-order logic programming language called λProlog
in collaboration with Dale Miller.
This language pioneered systematic support for
higher-order abstract syntax, a new way of viewing
the syntactic structure of objects such as programs, formulas, proofs
and types that occur in many symbol processing tasks.
I have subsequently led a research project that has developed the
Teyjus system that is an
efficient implementation of λProlog. Version 2 of this system
was released in April 2008 and runs on varied architectures and under
all the major operating systems.
The λProlog language provides as a mechanism for specifying
systems that can be conveniently conceptualized via a collection of
inference rules operating on the syntax of objects. I am interested
also in reasoning about the properties of such systems through their
specifications. The SLIMMER project initiated
the work of my group in this direction and resulted in the
Bedwyr
theorem-prover. We have subsequently started working on developing
more powerful reasoning
capabilities. The Abella system
embodies some of the foundational work we have done on designing
logics to support such reasoning.
My research also spans theoretical developments that are useful
relative to programming languages and logical frameworks. In the past,
such work has spanned proof theory and logic, lambda calculus
notations and their properties and unification procedures.
A note for prospective graduate students: I will be happy to exchange
mail about research interests and possibilities. However, I typically
do not respond to requests for funding that come without any prior
context. More importantly, you would be wasting your time and mine if
you try to indulge in such a discussion. Our department has an
admissions committee that must make the first decisions and research
funding is relevant only after a clear connection in interests has
been established.
Research Interests
I am interested in the design, use and implementation of
programming languages. I am also interested in logic, especially as it
underlies our understanding of programming formalisms and as it
informs our construction of general reasoning systems.
Research Opportunities for Students
If you are a student at the University of Minnesota, you enjoy
introspecting on programs and programming, you like the challenge of
thinking of theoretical issues and you are thrilled by the idea of
testing out your thinking by building systems, do get in touch with me
because we will sure have some common interests. This is not a message
only to graduate students: I especially like working with motivated
and interested undergraduates so you are welcome as well. To
participate effectively in the research of my group, you will, of
course, need to have an adequate background to complement your
inclination. I can help you figure out how to go about doing this;
typically you should think of doing the Programming Languages
and the Compilers courses that we offer in the department and
you should also have done or should plan on doing a logic course or
a course on computability theory.
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. We
typically decide on whether or not we are going to do this and also
the time for the meeting at the beginning of the semester so you
should get in touch with one of the Programming Languages and Software
Engineering faculty early enough if you are interested. 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.
Conference Program Committees
Editorial and Related Duties
Teaching
Current and Recent Courses
Some Older Courses