Typechecking is undecidable when 'type' is a type (1989) [pdf]
by zem on 1/30/2026, 5:31:29 AM
https://dspace.mit.edu/bitstream/handle/1721.1/149366/MIT-LCS-TR-458.pdf?sequence=6
Comments
by: moomin
It feels like this is unsurprising, given we already have Goedel's theorems and halting theorems. Any system of self-describing complexity ends up in this territory.
2/1/2026, 10:15:55 PM
by: Animats
This sounds close to Russell's "class of all classes" paradox. Is it?
2/1/2026, 8:48:29 PM
by: randomNumber7
And still this type system could be the base for a very interesting and powerfull programming language imo.
2/1/2026, 10:21:14 PM
by: cwmoore
Similar to the difficulty in finding Title Search companies on Indeed.
2/1/2026, 8:50:11 PM
by: marcosdumay
Hum... I'm getting 403, forbiden. Is it down?
2/1/2026, 9:05:13 PM