CERTIFIED PROGRAMMING WITH DEPENDENT TYPES

Abstract

The proposed work has two main tasks to link two seemingly different disciplines: Homotopy Type Theory and Quantum Programming Languages. In the first part of the proposal, the PI works toward developing a new Homotopy Type Theory-based proof assistant system that can internally formalize itself. In the second part of the proposal, the PI studies how dependent type theory can be used in quantum programming languages.

Document Details

Document Type
DoD Grant Award
Publication Date
Mar 23, 2016
Source ID
FA95501610029

Entities

People

  • Thorsten Altenkirch

Organizations

  • Air Force Office of Scientific Research
  • United States Air Force
  • University of Nottingham

Tags

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Operations Research
  • Research Science/Academic Research

Technology Areas

  • Quantum Computing