Birkedal, Lars; Clouston, Ranald; Mannaa, Bassel; Ejlers Møgelberg, Rasmus; Pitts, Andrew M.; Spitters, Bas Modal dependent type theory and dependent right adjoints. (English) Zbl 1479.03011 Math. Struct. Comput. Sci. 30, No. 2, 118-138 (2020). MSC: 03B38 03B40 03B45 18A40 PDFBibTeX XMLCite \textit{L. Birkedal} et al., Math. Struct. Comput. Sci. 30, No. 2, 118--138 (2020; Zbl 1479.03011) Full Text: DOI arXiv
Clouston, Ranald; Bizjak, Aleš; Grathwohl, Hans Bugge; Birkedal, Lars The guarded lambda-calculus: programming and reasoning with guarded recursion for coinductive types. (English) Zbl 1445.03012 Log. Methods Comput. Sci. 12, No. 3, Paper No. 7, 39 p. (2016). MSC: 03B40 68N18 PDFBibTeX XMLCite \textit{R. Clouston} et al., Log. Methods Comput. Sci. 12, No. 3, Paper No. 7, 39 p. (2016; Zbl 1445.03012) Full Text: DOI arXiv