HOMOTOPY TYPE THEORY AND PROBABILISTICCOMPUTATION
Abstract
This proposal will apply the new univalent foundation of mathematicsto computer science. More specifically, we will apply it to probabilisticprogramming with continuous data types, such as real numbers. Univalenthomotopy type theory connects homotopy type, algebraic topology and highercategory theory, with type theory and proof assistants. This exciting newfoundation both facilitates the development of mathematics, but also providesthe basis for a new generation of computer proof assistants. In these proofassistants one has more extensionality principles, which allows one to staycloser to mathematical practice, while at the same time programming in amore abstract, and thus modular, manner.We will use univalent homotopy type theory as a semantics for the implementationof probabilistic programming with continuous data types. In orderto do this, we will make progress on both realizability models, and on sheafmodels for homotopy type theory. More specifically, we will focus on Coquand’scubical type theory, which provides a computational interpretation ofVoevodsky’s univalence axiom. This is a next step in our current research program,which adds infinite objects to type theory, using the theory of guardedrecursion. We will provide a prototype implementation of this new type theory,either in the agda proof assistant, or in the Coq proof assistant.Next to this fundamental work, we will focus on the application of probabilisticprogramming and proof assistants to cryptography, in close collaborationwith leading cryptographers. In this way we aim to significantly expandthe reach of proof assistants.
Document Details
- Document Type
- DoD Grant Award
- Publication Date
- Jun 11, 2018
- Source ID
- FA95501810356
Entities
People
- Bas Spitters
Organizations
- Aarhus University
- Air Force Office of Scientific Research
- United States Air Force