Higher-Order Superposition for Dependent Types,

Abstract

In this paper we extend the higher-order critical pair criterion to the LF framework, a calculus with dependent types. The notion of dependence relation is introduced, and used to restrict rewriting to those cases where well-typedness is preserved.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 09, 1995
Accession Number
ADA306659

Entities

People

  • Roberto Virga

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Calculus
  • Computational Science
  • Computer Science
  • Conversion
  • Environment
  • Hierarchies
  • Hypotheses
  • Inversion
  • Judgment
  • Notation
  • Sequences
  • Two Dimensional

Readers

  • Computational Linguistics
  • Mechanical Engineering/Mechanics of Materials.