Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes.

Lars Birkedal, Rasmus Ejlers Mgelberg

Browse the full LICS paper archive.