Grant: Discovery Grants Program - Individual

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 physicsand 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.