Contextual Modal Type Theory with Polymorphic Contexts

Yuito Murase, Yuichi Nishiwaki, Atsushi Igarashi

Modal types -- types that are derived from proof systems of modal logic -- have been studied as theoretical foundations of metaprogramming, where program code is manipulated as fir…