Specialized Logics for Applications in Computer Science

Cornell University, Ithaca NY

Investigators

Abstract

This project is directed toward developing specialized logics for certain applications in computer science. The objective is to develop more efficient and effective modes of reasoning in particular instances by exploiting the special mathematical structure of the application. One would like to provide natural logical rules that match the problem at hand, thereby streamlining the reasoning process and making it more amenable to automation. Within this general context, five specific research projects are proposed, involving (1) Kleene algebra and Kleene algebra with tests; (2) binary relation, trace, and language models; (3) stochastic processes, probabilistic programs, and dynamical systems; (4) basic category theory; and (5) monads and monad composition. In each of these projects, new modes of reasoning or logical principles can be developed that take advantage of the particular mathematics of the problem to enhance the reasoning process. In some cases, automated tools based on these principles can be developed. For example, in (3), existing techniques for stochastic processes typically require heavy use of mathematical analysis. However, for certain arguments, one can give algebraic or logical proof principles that encapsulate the necessary analysis and allow reasoning to take place at a more abstract algebraic level. In (4), a new deductive system for arguments in basic category theory is proposed that will allow much of the process to be automated. Finally, in (5), one can give a new high-level approach to reasoning about monads and other categorical structures based on string rewriting. 2 Broader Impacts Resulting from the Proposed Activity The new intellectual tools proposed here can help shortcut complicated arguments and significantly increase reliability of complex systems. As the complexity of systems that we deal with increases from day to day, such tools are sorely needed. For example, monads have recently become very popular in functional and logic programming. They have been shown to provide a means to combine modules or extend functionality of programming languages or data structures with new features such as continuations, state, and concurrency. Monad composition proofs are notoriously involved, however. With the new techniques proposed in (5), researchers in those areas will find it easier to reason about monads and monad composition. The project will fully integrate research and education and provide significant opportunities for both undergraduate and graduate students for involvement in research and independent study. The project will enhance the infrastructure for research and education through the KATML system and software to be developed for basic category-theoretic reasoning. Both of these systems will promote intellectual rigor and provide students with a tool for understanding formal systems through experimentation. The KAT-ML system has already been used successfully in the undergraduate course on automata and computability at Cornell for working with regular expressions, and has proved to be quite popular.