A sound pure type system with ranks as sorts and Type-in-Type
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2610.25085
curl -X POST /api/v1/records/arxiv/2610.25085/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2610.25085/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'