Dependent Types and Explicit Substitutions

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Nov 01, 1999
Accession Number
ADA371144

Entities

People

  • Cesar Munoz

Tags

Communities of Interest

  • Space

DTIC Thesaurus Topics

  • Abstracts
  • Calculus
  • Classification
  • Computer Science
  • Computers
  • Confluence
  • Conversion
  • Engineering
  • Formal Languages
  • Grammars
  • Inversion
  • Judgment
  • Language
  • Notation
  • Programming Languages
  • Space Sciences
  • Standards

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.