SHF: SMALL: NONSTANDARD COMPUTATIONAL MODELS OF LINEAR LOGIC

SHF：小：线性逻辑的非标准计算模型

• 批准号: 1421193
• 负责人: Stephan Zdancewic
• 金额: $ 45万
• 依托单位: University of Pennsylvania
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2014
• 资助国家: 美国
• 起止时间: 2014-09-01 至 2019-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1421193&HistoricalAwards=false
• 关键词: SHF; SMALL; NONSTANDARD; COMPUTATIONAL; MODELS

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.

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