An Equational Logical Framework for Type Theories

Robert Harper

An Equational Logical Framework for Type Theories

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2106.01484 v1 pith:MLHZKTLT submitted 2021-06-02 math.LO cs.LO

An Equational Logical Framework for Type Theories

Robert Harper This is my paper

classification math.LO cs.LO

keywords typeframeworktheorieslogicalequalityequationalpresentedclass

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

0 comments

read the original 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.

discussion (0)

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Directed proof-relevant logical relations in simplicial HoTT
cs.LO 2026-07 accept novelty 7.5 partial

Contravariant families in simplicial HoTT supply proof-relevant expansion, yielding directed Boolean canonicity and a binary parametricity model over reduction-aware syntax.