This technical report investigates Kripke-style modal type theories, both simply typed and dependently typed. We examine basic meta-theories of the type theories, develop their substitution calculi, and give normalization by evaluation algorithms.

翻译：本技术报告调查了Kripke式模式型式理论,既简单打字,又依附打字。 我们研究了这类理论的基本元理论,开发替代计算法,并通过评估算法实现正常化。