Research Statement

Soon I recognized the tremendous difficulty hiding behind the area of general mathematics and I restricted myself to the domain of deductive systems which are already enormously expressive on their own, but better suited to study the problem. Deductive systems are commonly used to model programming languages, logics, and in general large parts of constructive mathematics. Constructive mathematics is important for my research program, because it equates provability with the existence of executable functions.

In order to use computers to develop programming languages and logics --- the objects I am working with --- one has to first represent them formally. For this matter I have chosen the logical framework LF, originally developed at the University of Edinburgh, which is now an active area of research at Carnegie Mellon. It is a higher-order type theory, elegant and concise, and its strength lies in its expressive power to represent deductive systems directly and adequately.

The main results of my current research are the design of a meta-logical framework extending LF which supports reasoning about deductive systems and an implementation of an automated theorem prover in the Twelf system which performs proof search. The system inherits its expressive power from the underlying logical framework, namely dependent types and higher-order representation principles which make appeals to substitution lemmas a primitive operation.

I have tackled several quite significant examples and have automatically shown --- using the Twelf system --- that intuitionistic logic and classical logic are sound, that the logic programming language based on the fragment of hereditary Harrop formulas is sound and complete with respect to uniform proof search, and that the Church-Rosser theorem holds for the untyped lambda-calculus. These are not new results, but they clearly demonstrate the scalability of the ideas behind my design.

My meta-logical framework is novel in that it rigorously separates between the representation level of LF and the meta level, on which the reasoning process takes place while taking advantage of the representation power of LF. It is general enough to support hypothetical arguments.

I am also eager to work with students, because I firmly believe that students are an important and vital part of a research project in a university setting. I find discussions with students and fellow researchers enormously stimulating because new ideas are always being created. Moreover I am convinced that one can reach a deep understanding of complicated concepts only by means of communication. This is one of the main reasons why I am looking for an academic position.

From a practical and specific point of view, I envision for example to contribute to the design of new programming languages, such as ML2000 or future versions of Java, to the design of new and safe protocols for computer networks, e-commerce, and authentication, and to the design of safe extensions for mobile code. I strongly believe that verifiable safety certificates should be part of every piece of code sent across the wire, and I see meta-logical frameworks as one of the key techniques to develop the theoretical foundations.

From a more theoretical point of view, I want to understand the requirements for a meta-logical framework stipulated by real world problems. I already foresee insufficiencies in the expressive power of traditional type theories when representing full programming languages or security protocols. In order to represent heap memory or protocol states in Twelf, one would like to employ features currently not provided by the underlying logical framework LF.

I anticipate working on questions such as: What features does a meta-logical framework have to offer to make it a good candidate to represent a programming language like Java? Is there a decidable unification algorithm for a natural fragment of the linear logical framework? What are the consequences of the aliasing problem to the choice and the design of a meta-logical framework? Which additional complications pose parallel programming languages? What is the representation of a trace of a protocol? I suspect that my results will be applicable to other areas of formal methods, such as model checking, in particular protocol verification, and hopefully to software engineering, in the form of specification languages to modularize software design.