Type Safe Multi-Stage Programming with Lys
Bachelor Thesis, University of Cambridge, 2023, with Jeremy Yallop, Alan Mycroft.
The work concerns the application of the simply typed version of contextual modal type theory (CMTT) to multi-stage programming (MSP). Specifically, we design and implement Lys, a MSP language based on CMTT. Then, we study its expressivity in comparison to other MSP paradigms like MetaOCaml by translating programs from MetaOCaml to Lys.