Type Theory, Computation and Interactive Theorem Proving

Abstract

Type theory is a logical formalism that is rich enough to express complex mathematical and computational assertions. In this project, Avigad and Harper developed type-theoretic algorithms and formalisms that can support the development of secure and reusable software libraries, as well as the development of methods of automated reasoning in mathematics and libraries of mathematical knowledge.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 2015
Accession Number
AD1003773

Entities

People

  • Jeremy Avigad
  • Robert Harper

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Engineered Resilient Systems

DTIC Thesaurus Topics

  • Abstracts
  • Air Force Research Laboratories
  • Algebraic Topology
  • Algorithms
  • Artificial Intelligence Computing
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Contracts
  • Electronic Mail
  • Language
  • Mathematics
  • Programming Languages
  • Reasoning
  • Topology

Readers

  • Computational Linguistics
  • Distributed Systems and Data Platform Development
  • Mathematical Modeling and Probability Theory.