3 Search Results for "Devriese, Dominique"

Document
DOI: 10.4230/LIPIcs.ECOOP.2025.2
The Algebra of Patterns

Authors: David Binder and Lean Ermantraut

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Pattern matching is a popular feature in functional, imperative and object-oriented programming languages. Language designers should therefore invest effort in a good design for pattern matching. Most languages choose a first-match semantics for pattern matching; that is, clauses are tried in the order in which they appear in the program until the first one matches. As a consequence, the order in which the clauses appear cannot be arbitrarily changed, which results in a less declarative programming model. The declarative alternative to this is an order-independent semantics for pattern matching, which is not implemented in most programming languages since it requires more verbose patterns. The reason for this verbosity is that the syntax of patterns is usually not expressive enough to express the complement of a pattern. In this paper, we show a principled way to make order-independent pattern matching practical. Our solution consists of two parts: First, we introduce a boolean algebra of patterns which can express the complement of a pattern. Second, we introduce default clauses to pattern matches. These default clauses capture the essential idea of a fallthrough case without sacrificing the property of order-independence.
Cite as

David Binder and Lean Ermantraut. The Algebra of Patterns. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 2:1-2:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{binder_et_al:LIPIcs.ECOOP.2025.2,
  author =	{Binder, David and Ermantraut, Lean},
  title =	{{The Algebra of Patterns}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{2:1--2:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.2},
  URN =		{urn:nbn:de:0030-drops-232959},
  doi =		{10.4230/LIPIcs.ECOOP.2025.2},
  annote =	{Keywords: functional programming, pattern matching, algebraic data types, equational reasoning}
}
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}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2024
  • 1 2021

  • Refine by Author
  • 2 Devriese, Dominique
  • 2 Nuyts, Andreas
  • 1 Binder, David
  • 1 Ceulemans, Joris
  • 1 Ermantraut, Lean
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs

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

  • Refine by Keyword
  • 1 Structural Operational Semantics
  • 1 algebraic data types
  • 1 dependent type theory
  • 1 distributive laws
  • 1 equational reasoning
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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