We introduce layers to modal type theories, which subsequently enables type theories for pattern matching on code in meta-programming and clean and straightforward semantics.

翻译：本文在模态类型理论中引入层（layers）结构，从而为元编程中代码的模式匹配提供类型理论支撑，并赋予其简洁清晰的语义。