DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2025.12

Nominal Type Theory by Nullary Internal Parametricity

Authors: Antoine Van Muylder, Andreas Nuyts, and Dominique Devriese

Published in: LIPIcs, Volume 384, 31st International Conference on Types for Proofs and Programs (TYPES 2025)

Abstract

There are many ways to represent the syntax of a language with binders. In particular, nominal frameworks are metalanguages that feature (among others) name abstraction types, which can be used to specify the type of binders. The resulting syntax representation, nominal data types, makes alpha-equivalent terms equal, has a closed induction principle and is well-behaved w.r.t. weakening. It is known that name abstraction types can be presented either as an existential or as a universal quantification on names. Existential name abstractions support matching on name-binding patterns but have cumbersome typing rules; universal ones have clean rules but apparently no such nominal matching. In this work we show that this matching ability and other nominal features are recovered in a type theory consisting of (1) Nullary (0-ary) Internally Parametric Type Theory (nullary PTT), (2) a type of names and a novel name induction principle, (3) nominal data types. This type theory is a legitimate nominal framework: it has universal and (non-primitive) existential name abstractions, a freshness type former, restricted name swapping and local-scope operations. Nominal pattern matching is recovered via term-relevant nullary parametricity. We provide an example involving synthetic Kripke parametricity.

Cite as

Antoine Van Muylder, Andreas Nuyts, and Dominique Devriese. Nominal Type Theory by Nullary Internal Parametricity. In 31st International Conference on Types for Proofs and Programs (TYPES 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 384, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{vanmuylder_et_al:LIPIcs.TYPES.2025.12,
  author =	{Van Muylder, Antoine and Nuyts, Andreas and Devriese, Dominique},
  title =	{{Nominal Type Theory by Nullary Internal Parametricity}},
  booktitle =	{31st International Conference on Types for Proofs and Programs (TYPES 2025)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-441-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{384},
  editor =	{Nordvall Forsberg, Fredrik and McKinna, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2025.12},
  URN =		{urn:nbn:de:0030-drops-270300},
  doi =		{10.4230/LIPIcs.TYPES.2025.12},
  annote =	{Keywords: Nominal techniques, Parametricity}
}

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.MFCS.2021.88

Abstract Congruence Criteria for Weak Bisimilarity

Authors: Stelios Tsampas, Christian Williams, Andreas Nuyts, Dominique Devriese, and Frank Piessens

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract

We introduce three general compositionality criteria over operational semantics and prove that, when all three are satisfied together, they guarantee weak bisimulation being a congruence. Our work is founded upon Turi and Plotkin’s mathematical operational semantics and the coalgebraic approach to weak bisimulation by Brengos. We demonstrate each criterion with various examples of success and failure and establish a formal connection with the simply WB cool rule format of Bloom and van Glabbeek. In addition, we show that the three criteria induce lax models in the sense of Bonchi et al.

Cite as

Stelios Tsampas, Christian Williams, Andreas Nuyts, Dominique Devriese, and Frank Piessens. Abstract Congruence Criteria for Weak Bisimilarity. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 88:1-88:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{tsampas_et_al:LIPIcs.MFCS.2021.88,
  author =	{Tsampas, Stelios and Williams, Christian and Nuyts, Andreas and Devriese, Dominique and Piessens, Frank},
  title =	{{Abstract Congruence Criteria for Weak Bisimilarity}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{88:1--88:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.88},
  URN =		{urn:nbn:de:0030-drops-145281},
  doi =		{10.4230/LIPIcs.MFCS.2021.88},
  annote =	{Keywords: Structural Operational Semantics, distributive laws, weak bisimilarity}
}

Search Results

Documents authored by Nuyts, Andreas

Nominal Type Theory by Nullary Internal Parametricity

Abstract

Cite as

A Sound and Complete Substitution Algorithm for Multimode Type Theory

Abstract

Cite as

Abstract Congruence Criteria for Weak Bisimilarity

Abstract

Cite as

Thanks for your feedback!

Could not send message