NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Press Enter or click the Search button to begin your search.

Back to Results
Dependent Types and Explicit SubstitutionsWe present a dependent-type system for a lambda-calculus with explicit substitutions. In this system, meta-variables, subject reduction, soundness, confluence and weak normalization.
Document ID
19990116988
Acquisition Source
Langley Research Center
Document Type
Contractor Report (CR)
Authors
Munoz, Ceasar
(Institute for Computer Applications in Science and Engineering Hampton, VA United States)
Date Acquired
September 6, 2013
Publication Date
November 1, 1999
Subject Category
Computer Programming And Software
Report/Patent Number
NASA/CR-1999-209722
NAS 1.26:209722
ICASE-99-43
Report Number: NASA/CR-1999-209722
Report Number: NAS 1.26:209722
Report Number: ICASE-99-43
Funding Number(s)
CONTRACT_GRANT: NAS1-97046
PROJECT: RTOP 505-90-52-01
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
No Preview Available