An Equational Logical Framework for Type Theories
Logic
2021-06-04 v1 Logic in Computer Science
Abstract
A wide range of intuitionistic type theories may be presented as equational theories within a logical framework. This method was formulated by Per Martin-L\"{o}f in the mid-1980's and further developed by Uemura, who used it to prove an initiality result for a class of models. Herein is presented a logical framework for type theories that includes an extensional equality type so that a type theory may be given by a signature of constants. The framework is illustrated by a number of examples of type-theoretic concepts, including identity and equality types, and a hierarchy of universes.
Keywords
Cite
@article{arxiv.2106.01484,
title = {An Equational Logical Framework for Type Theories},
author = {Robert Harper},
journal= {arXiv preprint arXiv:2106.01484},
year = {2021}
}