1 Search Results for "Stassen, Philipp"

Document

DOI: 10.4230/LIPIcs.TYPES.2022.6

{mitten}: A Flexible Multimodal Proof Assistant

Authors: Philipp Stassen, Daniel Gratzer, and Lars Birkedal

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract

Recently, there has been a growing interest in type theories which include modalities, unary type constructors which need not commute with substitution. Here we focus on MTT [Daniel Gratzer et al., 2021], a general modal type theory which can internalize arbitrary collections of (dependent) right adjoints [Birkedal et al., 2020]. These modalities are specified by mode theories [Licata and Shulman, 2016], 2-categories whose objects corresponds to modes, morphisms to modalities, and 2-cells to natural transformations between modalities. We contribute a defunctionalized NbE algorithm which reduces the type-checking problem for MTT to deciding the word problem for the mode theory. The algorithm is restricted to the class of preordered mode theories - mode theories with at most one 2-cell between any pair of modalities. Crucially, the normalization algorithm does not depend on the particulars of the mode theory and can be applied without change to any preordered collection of modalities. Furthermore, we specify a bidirectional syntax for MTT together with a type-checking algorithm. We further contribute mitten, a flexible experimental proof assistant implementing these algorithms which supports all decidable preordered mode theories without alteration.

Cite as

Philipp Stassen, Daniel Gratzer, and Lars Birkedal. {mitten}: A Flexible Multimodal Proof Assistant. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{stassen_et_al:LIPIcs.TYPES.2022.6,
  author =	{Stassen, Philipp and Gratzer, Daniel and Birkedal, Lars},
  title =	{{\{mitten\}: A Flexible Multimodal Proof Assistant}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{6:1--6:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.6},
  URN =		{urn:nbn:de:0030-drops-184498},
  doi =		{10.4230/LIPIcs.TYPES.2022.6},
  annote =	{Keywords: Dependent type theory, guarded recursion, modal type theory, proof assistants}
}

Refine by Author
1 Birkedal, Lars
1 Gratzer, Daniel
1 Stassen, Philipp

Refine by Classification

Refine by Keyword
1 Dependent type theory
1 guarded recursion
1 modal type theory
1 proof assistants

Refine by Type
1 document

Refine by Publication Year
1 2023

1 Search Results for "Stassen, Philipp"

{mitten}: A Flexible Multimodal Proof Assistant

Abstract

Cite as

Thanks for your feedback!

Could not send message