Equality Is Typable in Semi-full Pure Type Systems.

Vincent Siles, Hugo Herbelin

Browse the full LICS paper archive.