Layered Modal Type Theories

2023/05/11 by Jason Z. S. Hu, Hu, Jason Z. S., Brigitte Pientka +1
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Programming Languages (cs.PL)

paper · pdf · doi:10.48550/arxiv.2305.06548

openalex publication_date 2023/05/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We introduce layers to modal type theories, which subsequently enables type theories for pattern matching on code in meta-programming and clean and straightforward semantics.

Related

• DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
• Contextual Modal Type Theory with Polymorphic Contexts
• An Investigation of Kripke-style Modal Type Theories
• Graded Modal Dependent Type Theory
• Modality via Iterated Enrichment