{"id":"arxiv/2610.25085","url":"https://arxiv.org/abs/2610.25085","tags":["math.LO","cs.LO"],"score":0,"title":"A sound pure type system with ranks as sorts and Type-in-Type","domain":"math.LO","source":"arxiv","authors":["Pavel Sokolov","Alexander Kuklev"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-10-18","reactions":{}}