Mathesis: The Mathematical Foundation of Ulysses.

Abstract

This is an interim report for the Computer Security Properties Modeling Environment (ULYSSES) contract. This report is an introduction to MATHESIS, the underlying mathematical foundation for ULYSSES. The theory of constructions is a form of generalized type assignment to lambda-terms; hence, the paper begins with typed lambda-calculus and continues with the essentially equivalent idea of type assignment to untyped lambda-terms and its generalizations. Because the theory of constructions is also based on constructive logic and the notion of formulas-as-types, a chapter on this subject is included. With this expository preparation, the theory of constructions itself, along with its basic metatheory (including the strong normalization theory and some of its consequences) is taken up. The paper closes with a chapter on representing mathematics and logic in the theory of constructions. The mathematics presented is that which is relevant to the ULYSSES' theory of security.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 1987
Accession Number
ADA195379

Entities

People

  • Jonathan Seldin

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Arithmetic
  • Calculus
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Consistency
  • Construction
  • Cybersecurity
  • Language
  • Logic
  • Mathematical Logic
  • Mathematics
  • Programming Languages
  • Security
  • Set Theory

Fields of Study

  • Mathematics

Readers

  • Calculus or Mathematical Analysis
  • Computational Linguistics
  • Military History of the United States in the 20th Century.

Technology Areas

  • Cyber
  • Cyber - Cryptography