DeLaM: A Dependent Layered Modal Type Theory for Meta-programming

TL;DR

DeLaM is a novel dependent layered modal type theory that enables code composition, execution, and introspective analysis of code within a unified framework, supporting type-safe tactics in proof assistants.

Contribution

It introduces DeLaM, the first dependent layered modal type theory that combines code manipulation and introspection within a single sound framework.

Findings

Supports composition and execution of code

Enables introspective analysis of types and terms

Provides a foundation for type-safe tactics in proof assistants

Abstract

We scale layered modal type theory to dependent types, introducing DeLaM, dependent layered modal type theory. This type theory is novel in that we have one uniform type theory in which we can not only compose and execute code, but also intensionally analyze the code of types and terms. The latter in particular allows us to write tactics as meta-programs and use regular libraries when writing tactics. DeLaM provides a sound foundation for proof assistants to support type-safe tactic mechanism.