An Investigation of Kripke-style Modal Type Theories
arXiv:2206.07823
Abstract
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.