CS&E Profile: Gopalan Nadathur

Programming language design & implementation, declarative & specification languages, compilation techniques, and formal methods.

Ph.D. 1987, Computer Science, University of Pennsylvania

M.E. 1979, Automation, Indian Institute of Science, Bangalore, India

B.Tech. 1977, Electrical Engineering, Indian Institute of Technology, Kharagpur, India

About

Gopalan Nadathur has research interests in the design, application and implementation of programming languages. He also has research interests in logic, especially as it underlies the understanding of computation and the structure of programming formalisms and as it informs the construction of general reasoning systems.

Nadathur has made several well-recognized contributions in the realm of declarative programming. He is an inventor of a language called λProlog that pioneered a higher-order approach to computing with formal syntactic objects such as programs, formulas and proofs. He has developed an efficient compiler-based implementation of λProlog that has been used in several research projects around the world. He is also known for his work on the practical treatment of the lambda calculus and higher-order unification and on using proof-theoretic ideas in proof search and language design.

Nadathur has been a member of the faculty at Duke University and the University of Chicago and has held visiting appointments at the University of Munich, INRIA and Ecole Polytechnique. He has been the Steering Committee Chair for the International Conference on Principles and Practice of Declarative Programming and is a serving member of the Editorial Boards for Theory and Practice of Logic Programming and the Journal of Functional and Logic Programming.

Research

My research interests span the areas of computational logic and programming languages. The first area concerns the study of formalisms that can be used to describe and reason about the behavior of different kinds of objects and systems. Typical issues examined in this context are the expressiveness of chosen formalisms and the automation of the reasoning process. The second area is also concerned with formalisms, but this time from the perspective of encoding computations. The focus here is on devising new approaches to solving programming problems, designing languages to support these approaches and developing methods for implementing these languages that make it practical to use them.

There are many interacting themes between the two areas and my research recognizes and exploits this fact. In past work, my colleagues and I have developed a framework (that is now widely accepted) for using logical languages directly as a means for programming with the reasoning process playing the dual role of a computation mechanism. Using this framework in conjunction with a higher-order logic, I have developed a programming language called LProlog. This language supports a new way of representing and manipulating complex formal objects such as proofs that are now being used in models for secure, mobile computing. I have developed methods for realizing the new features of LProlog efficiently and have embedded these in a recently completed compiler and virtual machine based implementation of the language. Some of my implementation ideas have general applicability and have been used, for instance, in a widely distributed implementation of the ML language. Ongoing work focuses on further developing the LProlog system, refining implementation methods and, more broadly, in utilizing logic related ideas in programming.