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

我多年来的研究项目一直是理论计算机科学及其数学和逻辑基础。我的工作包括分析与现代编程语言理论相关的数学模型和许多形式逻辑。我们包括高阶逻辑、资源敏感线性逻辑以及证明的代数和拓扑结构以及证明网络等概念。这导致了我目前在证明即程序的动力学、反馈模型以及量子计算和量子测量理论的逻辑基础方面的研究。我们工作中的一个中心工具是范畴理论和范畴逻辑。*在这个研究方案中，我继续在三个相互关联的主题上扩展我之前的工作。主题1涉及多值逻辑及其代数，称为MV代数。这些令人着迷的逻辑是在20世纪20年代的S时期由逻辑学家发展起来的。在过去的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.