Pith. sign in

REVIEW 1 cited by

Quadratic type checking for objective type theory

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 2102.00905 v1 pith:BFDBEAOT submitted 2021-02-01 cs.LO

Benno van den Berg , Martijn den Besten This is my paper · ORCID
classification cs.LO
keywords typecheckingquadratictheorycomputationdefinitionaldoneeliminate
verification ladder T0 review T1 audit T2 compute T3 formal

Signed reviews

No signed human review yet.

0 comments
read the original abstract

We introduce a modification of standard Martin-Lof type theory in which we eliminate definitional equality and replace all computation rules by propositional equalities. We show that type checking for such a system can be done in quadratic time and that it has a natural homotopy-theoretic semantics.

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

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

  1. A 2-categorical approach to the semantics of dependent type theory with computation axioms

    math.LO 2025-07 conditional novelty 7.0 of 10

    A display map 2-category semantics for axiomatic type theory is shown sound, yielding a semantic proof that the identity type computation rule is not admissible.

Pith tools