## An Equational Formulation of LF

**R. Harper**
*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*

Previous |

Index |

Next