Computational Semantics of Cartesian Cubical Type Theory

Abstract

Dependent type theories are a family of logical systems that serve as expressive functional programming languages and as the basis of many proof assistants. In the past decade, type theories have also attracted the attention of mathematicians due to surprising connections with homotopy theory; the study of these connections, known as homotopy type theory, has in turn suggested novel extensions to type theory, including higher inductive types and Voevodskys univalence axiom. However, in their original axiomatic presentation, these extensions lack computational content, making them unusable as programming constructs and unergonomic in proof assistants.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 2019
Accession Number
AD1168009

Entities

People

  • Carlo Angiuli

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Calculus
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Construction
  • Judgment
  • Language
  • Mathematics
  • Monotone Functions
  • Notation
  • Numbers
  • Programming Languages
  • Set Theory
  • Theoretical Computer Science

Readers

  • Computational Linguistics
  • Graph Algorithms and Convex Optimization.
  • Theoretical Analysis.