Universes and relative indexed monads for type safe syntax and semantics

Jaro Reinders

Date: Wed, December 20, 2023
Time: 12:00
Room: Turing

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 |
Next: David Binder |