Accession Number:

ADA371144

Title:

Dependent Types and Explicit Substitutions

Descriptive Note:

Contractor rept.

Corporate Author:

INSTITUTE FOR COMPUTER APPLICATIONS IN SCIENCE AND ENGINEERING HAMPTON VA

Personal Author(s):

Report Date:

1999-11-01

Pagination or Media Count:

31.0

Abstract:

We present a dependent-type system for a lambda-calculus with explicit substitutions. In this system, meta-variables, as well as substitutions, are first-class objects. We show that the system enjoys properties like type uniqueness, subject reduction, soundness, confluence and weak normalization.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE