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
Distribution Statement : APPROVED FOR PUBLIC RELEASE