Accession Number : ADA306659

Title :   Higher-Order Superposition for Dependent Types,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Virga, Roberto

PDF Url : ADA306659

Report Date : 09 MAY 1995

Pagination or Media Count : 35

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.

Descriptors :   *COMPUTER PROGRAMMING, *MATHEMATICAL PROGRAMMING, COMPUTER LOGIC, RULE BASED SYSTEMS, SYSTEMS ANALYSIS, CALCULUS.

Subject Categories : Operations Research
      Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE