Skip to content
DraconiticResearch
Search Sources API
182,544 studies31 sourcesUpdated 3 min ago
PreprintarXiv licencearXiv

A sound pure type system with ranks as sorts and Type-in-Type

  • Pavel Sokolov
  • Alexander Kuklev
Open at sourcePDFDOICite

Abstract

We present a dependently typed pure type system that contains a circular axiom $s : s$ for a certain sort s and is nonetheless strongly normalizing. Girard's paradox is avoided because our sorts are not closed under a Π-former: function types are placed in sorts according to their rank. Turns out that this system has a unique set of characteristics: it has similar normalization behaviour as STLC (so complexity of normalization is TOWER-complete) while at the same time allowing non-uniform representation of arbitrary elementary recursive functions; furthermore, it has a nontrivial set-theoretical model in ZF+GCH and allows to carry out nontrivial proof developments. Base normalization proof is surprisingly simple (modulo general metatheoretical properties of pure type systems) and has been fully formalized in vanilla Rocq (formerly Coq) without additional axioms.

Related

  1. Pure Type-One Generalized Hypercomplex Structures in Dimension Four
    Guangzhen Ren
    arXivPreprintarXiv licenceFull textGeometry & topologyarXiv
  2. Borel's computation of the ranks of K-theory revisited
    Jan Ole Hesse
    arXivPreprintarXiv licenceFull textAlgebra & number theoryarXiv
  3. Optimal solution ranks in the Max-Cut semidefinite relaxation
    Avinash Bhardwaj, Vishnu Narayanan
    arXivPreprintCC BY 4.0Full textCombinatorics & discrete mathematicsOptimisation & controlarXiv
  4. Optimal Actuator Design across Ranks and Control Horizons
    Emmanuel Trélat, Enrique Zuazua
    HALPreprintPublisher termsFull textOptimisation & controlHALarXiv
  5. Ranks of Verdier quotients of derived categories over local rings
    Souvik Dey, Yuki Mifune
    arXivPreprintarXiv licenceFull textAlgebra & number theoryarXiv

Cite

BibTeXRIS
BibTeX
@misc{sokolov2026sound,
  title = {{A sound pure type system with ranks as sorts and Type-in-Type}},
  author = {Pavel Sokolov and Alexander Kuklev},
  howpublished = {arXiv},
  year = {2026},
  month = oct,
  doi = {10.48550/arxiv.2610.25085},
  eprint = {2610.25085},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2610.25085},
}
RIS
TY  - UNPB
TI  - A sound pure type system with ranks as sorts and Type-in-Type
AU  - Pavel Sokolov
AU  - Alexander Kuklev
PY  - 2026
DA  - 2026/10/18
PB  - arXiv
DO  - 10.48550/arxiv.2610.25085
UR  - https://arxiv.org/abs/2610.25085
AB  - We present a dependently typed pure type system that contains a circular axiom $s : s$ for a certain sort s and is nonetheless strongly normalizing. Girard's paradox is avoided because our sorts are not closed under a Π-former: function types are placed in sorts according to their rank. Turns out that this system has a unique set of characteristics: it has similar normalization behaviour as STLC (so complexity of normalization is TOWER-complete) while at the same time allowing non-uniform representation of arbitrary elementary recursive functions; furthermore, it has a nontrivial set-theoretical model in ZF+GCH and allows to carry out nontrivial proof developments. Base normalization proof is surprisingly simple (modulo general metatheoretical properties of pure type systems) and has been fully formalized in vanilla Rocq (formerly Coq) without additional axioms.
ER  -