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