paraconsistent type theory

Stream: Type theory

[Tim Slechten]

Recently, I have been learning type theory, and I find the usual techniques of avoiding Girard's paradox extremely unsatisfying. Solutions like "Type universes" and "strong normalization" introduce significant complexity while being overly restrictive. I think I may have found a simpler alternative: modifying the Curry-Howard correspondence to admit only normal forms as proofs. Thoughts? https://timslechten395.github.io/blog/posts/a-paraconsistent-type-theory/

[Kevin Buzzard]

This doesn't appear to be lean-related so is probably off-topic for this zulip instance.

[Tim Slechten]

sorry, this article is indeed unrelated to lean. It is more about type theory in general. I posted it here because this is the only type theory/formal verification community I know. Any suggestions on where to post it instead?

[Matt Diamond]

what about https://typ.zulipchat.com ?

[Matt Diamond]

FYI, here was my process: I googled "type theory mailing list", clicked through to the TYPES e-mail list and then saw there was a link to a Zulip (though the link was broken, I was able to figure it out from the mangled URL)

[Matt Diamond]

the Zulip doesn't seem to be very active, unfortunately (perhaps you're already aware of it?)

[Kevin Buzzard]

There is also the FOM mailing list (which is reasonably active).

[suhr]

Consider

example: (2).pow 64 = (2).pow 64 := rfl

It will take quite a while to compute the normal form (with numbers of form Nat.zero.succ.succ...) of this type.

[Tim Slechten]

Thanks for the suggestions, I'll check them out.

[Tim Slechten]

Only the terms need to be normalized, not types. You do not have to normalize every term either, proving that a normal form exists is enough. Normalizing is just a good default for the type checker because it always works.