• People
• Events
• Research

An Equational Formulation of LF

Abstract: This report outlines an equational variant of the LF type theory. We define a formal system for deriving equations from a set of equational hypotheses. We then give a definition of environment model suitable for systems of dependent types, and sketch a proof of soundness and (strong) completeness for the equational theory with respect to the class of environment models.

LFCS report ECS-LFCS-88-67