DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911947872534528 |
|---|---|
| author | Hu, Jason Z. S. Pientka, Brigitte |
| author_facet | Hu, Jason Z. S. Pientka, Brigitte |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_17065 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | DeLaM: A Dependent Layered Modal Type Theory for Meta-programming Hu, Jason Z. S. Pientka, Brigitte Logic in Computer Science Programming Languages 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. |
| title | DeLaM: A Dependent Layered Modal Type Theory for Meta-programming |
| topic | Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2404.17065 |