I am aware that assigning the type of Type to be Type (rather than stratifying to a hierarchy of types) leads to an inconsistency. But does this inconsistency allow the construction of a welltyped term with no normal form, or does it actually allow a proof of False? Are these two questions equivalent?
2 Answers
Girard's paradox constructs a nonnormalizing proof of False. You could read Hurken's "A simplification of Girard's paradox", or maybe Kevin Watkin's formalization in Twelf.
In general, these questions are not equivalent, though they often coincide. A "reasonable" type theory will by inspection have no normal proofs of False, and so then normalization implies consistency. The inverse (nonnormalization => proof of False) is much less obvious, and it is certainly possible to construct reasonable paraconsistent type theories, where nontermination is confined under a monad and does not result in a proof of False.

$\begingroup$ Do you have any references for the kind of paraconsistent type theory that you mention here? $\endgroup$ Oct 23, 2018 at 20:16

1$\begingroup$ see work on the "Delay monad" for type theories where nontermination (and hence proof of False) is confined under a monad. $\endgroup$ Oct 31, 2018 at 17:44
It leads to a welltyped term, having no normal form, which is assigned the type False. You can find the term given explicitly in A simplification of Girard's paradox

7$\begingroup$ Here's a free version of the linked paper: cs.cmu.edu/~kw/scans/hurkens95tlca.pdf $\endgroup$– erdesztNov 2, 2015 at 20:48