Universes and relative indexed monads for type safe syntax and semantics

Jaro Reinders

In this presentation, we’re taking a look at syntax representations such as De Bruijn indices and HOAS and their type safe variants. We look at conversions between these representations. Finally, we apply what we learn to free monad representations, ending up with a free relative indexed monad.

---

Previous: Valentin Bogad | ​Julia, types, and property based testing
Next: David Binder | Symmetric Dependent Data and Codata Types