Accession Number : ADA195379

Title :   Mathesis: The Mathematical Foundation of Ulysses.

Descriptive Note : Interim rept. Apr 85-Apr 87,

Corporate Author : ODYSSEY RESEARCH ASSOCIATES INC ITHACA NY

Personal Author(s) : Seldin, Jonathan

PDF Url : ADA195379

Report Date : Nov 1987

Pagination or Media Count : 165

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.

Descriptors :   *MATHEMATICAL PROGRAMMING, CONSTRUCTION, MATHEMATICS, NORMALIZING(STATISTICS), DATA PROCESSING SECURITY

Subject Categories : Theoretical Mathematics
      Computer Systems

Distribution Statement : APPROVED FOR PUBLIC RELEASE