Project Proposal Phase 1

I will be working with Jon Sterling on the denotational semantics of effectful languages with mixed evaluation-order (CBV/CBN). Specifically, I hope to be working on the univalent formalisation of various category-theoretic constructs – e.g. duploids, Freyd categories, and thunk-force categories – which are useful for reasoning about the semantics of such languages. I plan to use (and contribute to?) the Rocq UniMath library. More details later!