Specialized Logics for Applications in Computer Science

该项目旨在为计算机科学中的某些应用开发专门的逻辑。目的是利用应用程式的特殊数学结构，在特定情况下发展更有效率和更有效的推理模式。人们希望提供与手头问题相匹配的自然逻辑规则，从而简化推理过程，使其更易于自动化。在这个大背景下，提出了五个具体的研究项目，涉及（1）Kleene代数和带测试的Kleene代数;（2）二元关系、迹和语言模型;（3）随机过程、概率程序和动力系统;（4）基本范畴论;（5）单子和单子组合。在每一个项目中，可以开发新的推理模式或逻辑原则，利用问题的特定数学来增强推理过程。在某些情况下，可以开发基于这些原则的自动化工具。例如，在（3）中，现有的随机过程技术通常需要大量使用数学分析。然而，对于某些论点，人们可以给出代数或逻辑证明原则，这些原则封装了必要的分析，并允许在更抽象的代数层次上进行推理。在（4）中，提出了一个新的基本范畴论中的论证演绎系统，它将允许大部分过程自动化。最后，在（5）中，我们可以给出一个新的高级方法来推理单子和其他基于字符串重写的范畴结构。2提议的活动产生的更广泛的影响这里提出的新的智能工具可以帮助简化复杂的论点，并显着提高复杂系统的可靠性。随着我们处理的系统的复杂性日益增加，这些工具是非常需要的。例如，monad最近在函数和逻辑编程中变得非常流行。它们已经被证明提供了一种方法来联合收割机模块或扩展功能的编程语言或数据结构与新的功能，如延续，状态和并发。然而，Monad复合证明是众所周知的。采用（5）中提出的新技术，该项目将把研究和教育完全结合起来，为本科生和研究生提供参与研究和独立学习的重要机会。该项目将通过KATML系统和为基本类别开发的软件加强研究和教育的基础设施。理论推理。这两个系统都将促进智力的严谨性，并为学生提供一个通过实验来理解正式系统的工具。KAT-ML系统已经在康奈尔大学自动机和可计算性的本科课程中成功地使用正则表达式，并已被证明是非常受欢迎的。

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 placeat 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 ActivityThe 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 proposedin (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 opportunitiesfor both undergraduate and graduate students for involvement in research and independentstudy.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.