A course project investigating guarded recursion, guarded type theory, and denotational semantics.
- A presentation on the subject
- An agda formalization of the paper: Paviotti, Marco, Rasmus Ejlers Møgelberg, and Lars Birkedal. "A model of PCF in guarded type theory." Electronic Notes in Theoretical Computer Science 319 (2015): 333-349.
- A technical report on the project