ALP Exec Committee Nomination Statement

Dale Miller has been nominated to stand for election for the Executive Committee of the Association for Logic Programming (ALP). Voting should take place during Nov/Dec 2004.

Brief Statement

My focus at research will be echoed in my priorities while on the ALP Executive Committee.

Research foci

I have been working for close to twenty years on using logic to specify computation and to reason about such specifications. Finding first-order Horn clauses far too weak and inexpressive for that work, I have worked with a number of colleagues on more expressive logics bases on higher-order quantification and intuitionistic and linear logics. We have also worked at trying to find a general framework, based on the completeness of goal-direct search, to (partially) answer the question: When is a logic appropriate for logic programming? The lambda Prolog programming language has been a result of this work, as are the linear logic programming languages Lolli and Forum.

More recently, my research has focused on developing meta-logics and tools for reasoning about logic specifications (in the above-mentioned logic programming languages). Some of my most recent work addresses the correctness of security protocols and proving theorems about specifications languages such as the pi-calculus.

Executive Comm foci

I would like to see logic and declarative foundations play a central role in the future of the Logic Programming community. By emphasizing more logic, one may need to deemphasize programming with logic: one may have to give up the dream that everyone will eventually abandon C++ and Java for a logic programming language. Instead, logic programming can contribute to approaches and infrastructures that support correct and secure computation systems. Type inference, static analysis, program transformation, model checking, proof checking, and theorem proving are all areas in which logic programming can play significant roles. For example, the Proof Carrying Code paradigm makes central use of logic programming technology to provide flexible representation and checking of proofs and assertions. Proposals to add more and more declarative information to the binary outputs of compilers means that compiling, checking, moving, and loading of code will need deduction at every stage: such deduction is just the kind of thing the logic programming community can offer.

References

Miller's home page, a list of his recent papers, and his CV.