An Investigation of Kripke-style Modal Type Theories

2022/06/15 by Jason Z. S. Hu, Hu, Jason Z. S., Brigitte Pientka +1
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Natural Language Processing Techniques #Programming Languages (cs.PL)

paper · pdf · doi:10.48550/arxiv.2206.07823

openalex publication_date 2022/06/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related

• Layered Modal Type Theories
• Normalization for multimodal type theory
• DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
• A meta-modal logic for bisimulations
• First-Order Modal ξ-Calculus: On the Aspects of Application and Bisimulation