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 information-intensive infrastructure protection. We describe the rationale for this approach in this report.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 23, 2004
Accession Number
ADA426580

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

  • Mathematical Modeling and Probability Theory.
  • Software Engineering.