Homotopy Type Theory: CMU Research Group

Abstract

This one-year proposal is to add fund to the PI s MURI Award, FA9550-15-1-0053, to augment the original statement of work. In this added statement of work, the team will investigate Cubical Type Theory (a refinement model of Homotopy Type Theory), "synthetic" approach to the traditional homotopy theory, and further develop a new proof-assistant Lean in collaboration with a Microsoft Researcher.

Document Details

Document Type
DoD Grant Award
Publication Date
Feb 06, 2017
Source ID
FA95501710122

Entities

People

  • Steve Awodey

Organizations

  • Air Force Office of Scientific Research
  • Massachusetts Institute of Technology
  • United States Air Force

Tags

Readers

  • Mathematical Modeling and Probability Theory.
  • Research Science/Academic Research
  • Software Engineering.