Building Interactive Digital Libraries of Formal Algorithmic Knowledge

Abstract

This is a project to design and create a software system for sharing formal algorithmic mathematics among theorem provers, and for making formal algorithmic mathematics accessible to people who value verified accounts of algorithms. The project is also committed to creating interesting specimens of formally explained algorithms. Our work enables a new approach to CIP/SW; we call it information-intensive infrastructure protection. We describe the rationale for this approach in this report.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 2003
Accession Number
ADA414364

Entities

People

  • Robert L. Constable

Organizations

  • Cornell University

Tags

Communities of Interest

  • C4I
  • Energy and Power Technologies
  • Human Systems

DTIC Thesaurus Topics

  • Acquisition
  • Algorithms
  • Arithmetic
  • Computer Programming
  • Computer Science
  • Computers
  • Cybersecurity
  • Engineering
  • Infrastructure
  • Language
  • Mathematics
  • Network Computing
  • Numbers
  • Programming Languages
  • Software Development
  • Students
  • Theorems

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Software Engineering.