SHF: SMALL: NONSTANDARD COMPUTATIONAL MODELS OF LINEAR LOGIC

标题：SHF：小型：线性逻辑的非标准计算模型今天开发的许多有趣的软件依赖于数学基础，这些基础可以最好地用线性代数（例如大规模矩阵或图形数据）和统计学（例如机器学习算法或“大数据”分析）来表达。目前的编程语言并不是特别适合处理这类数据，因此为科学家和软件开发人员提供的内置支持很少。相反，在线性代数和统计学的背景下已经开发了许多强大的数学技术，但这些技术并不适用于编程语言语义中的问题。该研究项目旨在建立一个理论基础，将看似不同的编程语言主题与这些数学领域联系起来。在这项工作中采用的技术方法是开发线性逻辑的“非标准”模型，这是一个用于理解程序语义的表达性和低级框架。智力上的优点是在已建立但不同的数学领域之间建立新的联系，将证明理论和程序语义与向量空间和概率测度类别中的表示联系起来。这项工作的广泛影响最好通过其潜在的长期应用来理解，其中包括：用于处理数值数据（如Matlab）的编程语言结构与支持高阶函数和抽象数据类型的平滑集成；基于数值方法的证明搜索新技术更好的编程语言来表达机器学习或概率算法。

TItle: SHF: Small: Nonstandard Computational Models of Linear LogicMuch of the interesting software being developed today relies on mathematical underpinnings that can best be expressed in terms of linear algebra (e.g. large scale matrices or graph data) and statistics (e.g. machine learning algorithms or "big data" analysis). Current programming languages aren't especially suited to working with such kinds of data, and so provide little built-in support to help scientists and software developers. Conversely, many powerful mathematical techniques have been developed in the contexts of linear algebra and statistics, but those techniques have not been applicable to problems in programming language semantics. This research project seeks to develop a theoretical foundation that connects the seemingly disparate topics of programming languages and these mathematical domains.The technical approach taken in this work is to develop "nonstandard" models of linear logic, which is an expressive and low-level framework for understanding program semantics. The intellectual merits are found in developing novel connections between well-established, but distinct, mathematical domains, connecting proof theory and program semantics to representations in vector spaces and categories of probability measures. The broader impacts of this work are best understood through its potential long-term applications, which include: smooth integration of programming language constructs for working with numerical data (like Matlab) with support for higher-order functions and abstract datatypes; new techniques for proof search based on numerical methods; and, better programming languages for expressing machine learning or probabilistic algorithm.