An Investigation of Kripke-style Modal Type Theories
Logic in Computer Science
2023-05-12 v5 Programming Languages
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.
Keywords
Cite
@article{arxiv.2206.07823,
title = {An Investigation of Kripke-style Modal Type Theories},
author = {Jason Z. S. Hu and Brigitte Pientka},
journal= {arXiv preprint arXiv:2206.07823},
year = {2023}
}