2 Search Results for "Stassen, Philipp"

Document
DOI: 10.4230/LIPIcs.TYPES.2023.4
A Sound and Complete Substitution Algorithm for Multimode Type Theory

Authors: Joris Ceulemans, Andreas Nuyts, and Dominique Devriese

Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)

Abstract
Multimode Type Theory (MTT) is a generic type theory that can be instantiated with an arbitrary mode theory to model features like parametricity, cohesion and guarded recursion. However, the presence of modalities in MTT significantly complicates the substitution calculus of this system. Moreover, MTT’s syntax has explicit substitutions with an axiomatic system - not an algorithm - governing the connection between an explicitly substituted term and the resulting term in which variables have actually been replaced. So far, the only results on eliminating explicit substitutions in MTT rely on normalisation by evaluation and hence also immediately normalise a term. In this paper, we present a substitution algorithm for MTT that is completely separated from normalisation. To this end, we introduce Substitution-Free Multimode Type Theory (SFMTT): a formulation of MTT without explicit substitutions, but for which we are able to give a structurally recursive substitution algorithm, suitable for implementation in a total programming language or proof assistant. On the usual formulation of MTT, we consider σ-equality, the congruence generated solely by equality rules for explicit substitutions. There is a trivial embedding from SFMTT to MTT, and a converse translation that eliminates the explicit substitutions. We prove soundness and completeness of our algorithm with respect to σ-equivalence and thus establish that MTT with σ-equality has computable σ-normal forms, given by the terms of SFMTT.
Cite as

Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. A Sound and Complete Substitution Algorithm for Multimode Type Theory. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{ceulemans_et_al:LIPIcs.TYPES.2023.4,
  author =	{Ceulemans, Joris and Nuyts, Andreas and Devriese, Dominique},
  title =	{{A Sound and Complete Substitution Algorithm for Multimode Type Theory}},
  booktitle =	{29th International Conference on Types for Proofs and Programs (TYPES 2023)},
  pages =	{4:1--4:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-332-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{303},
  editor =	{Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.4},
  URN =		{urn:nbn:de:0030-drops-204826},
  doi =		{10.4230/LIPIcs.TYPES.2023.4},
  annote =	{Keywords: dependent type theory, modalities, multimode type theory, explicit substitutions, substitution algorithm}
}
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 Ceulemans, Joris
  • 1 Devriese, Dominique
  • 1 Gratzer, Daniel
  • 1 Nuyts, Andreas
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Modal and temporal logics
  • 2 Theory of computation → Type theory
  • 1 Software and its engineering → Syntax

  • Refine by Keyword
  • 1 Dependent type theory
  • 1 dependent type theory
  • 1 explicit substitutions
  • 1 guarded recursion
  • 1 modal type theory
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2023
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact