Studies in many-valued logics, partial traces, and computability

多年来，我的研究项目一直是理论计算机科学及其数学和逻辑基础。我的工作包括分析数学模型和许多与现代编程语言理论相关的形式逻辑。我们包括这样的概念，高阶逻辑，资源敏感的线性逻辑，以及代数和拓扑结构的证明和网络的证明。这导致了我目前的研究在证明作为程序的动力学，反馈模型，量子计算和量子测量理论的逻辑基础。 我们工作中的一个核心工具是范畴理论和范畴逻辑。在这个研究计划中，我继续在三个相互关联的主题中扩展我以前的工作。 主题1涉及多值逻辑及其代数，称为MV代数。这些迷人的逻辑是由逻辑学家在20世纪20年代发展起来的。 在过去的30年里，MV代数被证明与当前数学的几个研究领域以及计算机科学和物理学有着显着的联系。 在20世纪90年代，从事量子测量和量子概率论的数学物理学家发展了量子效应的代数。令人惊讶的是，这些效应代数竟然包括MV代数。 我的工作（与同事在爱丁堡）开发了一个通用的表示和分类（或“协调”）计划MV和效果代数，使用某些半群所产生的算子代数。我的学生和我将继续协调程序分类MV代数使用半群共同的物理 * 和理论计算机科学，与应用等领域：无限自动机，概率逻辑和编程语言语义。 主题2研究部分反馈，包括递归和编程语言理论中的不动点。 我和我的学生开发了部分追踪范畴的一般理论（用于分析线性逻辑证明理论中的反馈），其中包含许多数学模型。我们继续寻找由量子信息理论激发的新模型（例如在某些C*-代数中）。未来的方向包括分析模拟计算基础中的度量空间模型，研究具有延迟的反馈，以及分析具有不动点算子的MV-代数（主题1）。主题3是一个长期项目。它研究了可计算性理论的新基础：图灵范畴（由R。Cockett和P. Hofstra）。 一个关键特性是使用形式化方法（在Coq中）来形式化相关的证明。这是形式化数学的一部分。研究的理论将包括从资源有界逻辑，高阶计算，以及从线性逻辑中的组合代数产生的模型的可计算函数。实际项目将包括正规安全方面的研究。

My research program for many years has been in theoretical computer science and its mathematical and logical foundations. My work involves analyzing the mathematical models and the many formal logics related to modern programming language theory. We include such notions as higher-order logics, resource sensitive linear logics, as well as the algebraic and topological structure of proofs and networks of proofs. This leads to my current studies in the dynamics of proofs-as-programs, models of feedback, and the logical foundations of quantum computing and quantum measurement theory. A central tool in our work is category theory and categorical logic.******In this research proposal, I continue to extend my previous work in three interlocking themes. Theme 1 involves many-valued logics and their algebras, called MV algebras. These fascinating logics were developed by logicians during the 1920's. In the last 30 years, MV algebras were shown to have remarkable connections to several current research areas of mathematics, as well as to computer science and physics. In the 1990s, mathematical physicists working in quantum measurement and quantum probability theories developed algebras of quantum effects. Surprisingly, these effect algebras turn out to include MV algebras. My work (with colleagues in Edinburgh) develops a general representation and classification (or “coordinatization”) program for MV and Effect algebras, using certain semigroups arising from operator algebras. My students and I will continue the coordinatization program to classify MV algebras using semigroups common to both physics***and theoretical computer science, with applications to such areas as: infinite automata, probabilistic logics, and programming language semantics. Theme 2 studies partial feedback, including recursion and fixed-points in programming language theory. My students and I developed a general theory of partially traced categories (for analyzing feedback in linear logic proof theory), with many mathematical models. We continue to look for new models motivated by quantum information theory (e.g. in certain C*-algebras). Future directions include analysis of metric space models in the foundations of analog computing, studying feedback with delay, and analysis of MV-algebras with fixed-point operators (in Theme 1). Theme 3 is a long-term project. It studies new foundations of computability theory: Turing categories (by R. Cockett and P. Hofstra). A key feature will be using formal methods (in Coq) to formalize the relevant proofs. This is part of formalized mathematics. Theories studied will include computable functions from resource bounded logics, higher-order computation, and models arising from combinatory algebras in linear logic. Practical projects will include studies in formal security.