10 Search Results for "Maggesi, Marco"

Artifact
Software
DOI: 10.4230/artifacts.25484
HOLMS: A HOL Light Library for Modal Systems

Authors: Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi

Abstract
Cite as

Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi. HOLMS: A HOL Light Library for Modal Systems (Software, Source code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-25484,
   title = {{HOLMS: A HOL Light Library for Modal Systems}}, 
   author = {Bilotta, Antonella and Maggesi, Marco and Perini Brogi, Cosimo},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:36edca29f53f3fdd0a7fc675702990743eda4c8d}{\texttt{swh:1:dir:36edca29f53f3fdd0a7fc675702990743eda4c8d}} (visited on 2026-02-18)},
   url = {https://github.com/HOLMS-lib/HOLMS},
   doi = {10.4230/artifacts.25484},
}
Artifact
Software
DOI: 10.4230/artifacts.25485
Webpage of HOLMS: A HOL Light Library for Modal Systems

Authors: Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi

Abstract
Cite as

Antonella Bilotta, Marco Maggesi, Cosimo Perini Brogi. Webpage of HOLMS: A HOL Light Library for Modal Systems (Software, Project Documentation Website). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{holms-website,
   title = {{Webpage of HOLMS: A HOL Light Library for Modal Systems}}, 
   author = {Bilotta, Antonella and Maggesi, Marco and Perini Brogi, Cosimo},
   note = {Software (visited on 2026-02-18)},
   url = {https://holms-lib.github.io/},
   doi = {10.4230/artifacts.25485},
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.18
A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light

Authors: Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
We extend the existing HOL Light Library for Modal Systems (HOLMS) to support a modular implementation of modal reasoning within the HOL Light proof assistant. We deeply embed axiomatic calculi and relational semantics for seven normal modal logics (K, T, B, K4, S4, S5, GL) and formalise modal adequacy theorems for these systems. We then leverage those formalisations to implement a mechanism for automated reasoning via proof-search in the associated labelled sequent calculi, which we shallowly embed in HOL Light’s goal-stack mechanism. This way, we equip the general-purpose proof assistant with (semi)decision procedures for these logics that, in case of failure to construct a proof for the input formula, return a certified countermodel within the appropriate class for the logic under consideration. On the methodological side, we propose a precise measure of the modularity of our approach by systematically adopting Christopher Strachey’s distinction between ad hoc and parametric polymorphism throughout the library.
Cite as

Antonella Bilotta, Marco Maggesi, and Cosimo Perini Brogi. A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 18:1-18:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{bilotta_et_al:LIPIcs.CSL.2026.18,
  author =	{Bilotta, Antonella and Maggesi, Marco and Perini Brogi, Cosimo},
  title =	{{A Modular Framework for Proof-Search via Formalised Modal Completeness in HOL Light}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{18:1--18:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.18},
  URN =		{urn:nbn:de:0030-drops-254427},
  doi =		{10.4230/LIPIcs.CSL.2026.18},
  annote =	{Keywords: Modal logic, HOL Light, Labelled sequent calculi, Logical verification, Interactive theorem proving, Automated proof-search}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.33
Scott’s Representation Theorem and the Univalent Karoubi Envelope

Authors: Arnoud van der Leer, Kobe Wullaert, and Benedikt Ahrens

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Lambek and Scott constructed a correspondence between simply-typed lambda calculi and Cartesian closed categories. Scott’s Representation Theorem is a cousin to this result for untyped lambda calculi. It states that every untyped lambda calculus arises from a reflexive object in some category. We present a formalization of Scott’s Representation Theorem in univalent foundations, in the (Rocq-)UniMath library. Specifically, we implement two proofs of that theorem, one by Scott and one by Hyland. We also explain the role of the Karoubi envelope - a categorical construction - in the proofs and the impact the chosen foundation has on this construction. Finally, we report on some automation we have implemented for the reduction of λ-terms.
Cite as

Arnoud van der Leer, Kobe Wullaert, and Benedikt Ahrens. Scott’s Representation Theorem and the Univalent Karoubi Envelope. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanderleer_et_al:LIPIcs.ITP.2025.33,
  author =	{van der Leer, Arnoud and Wullaert, Kobe and Ahrens, Benedikt},
  title =	{{Scott’s Representation Theorem and the Univalent Karoubi Envelope}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{33:1--33:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.33},
  URN =		{urn:nbn:de:0030-drops-246318},
  doi =		{10.4230/LIPIcs.ITP.2025.33},
  annote =	{Keywords: Lambda calculi, algebraic theories, categorical semantics, Karoubi envelope, formalization, Rocq-UniMath, univalent foundations}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2024.6
Data Types with Symmetries via Action Containers

Authors: Philipp Joram and Niccolò Veltri

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

Abstract
We study two kinds of containers for data types with symmetries in homotopy type theory, and clarify their relationship by introducing the intermediate notion of action containers. Quotient containers are set-valued containers with groups of permissible permutations of positions, interpreted as (possibly non-finitary) analytic functors on the category of sets. Symmetric containers encode symmetries in a groupoid of shapes, and are interpreted accordingly as polynomial functors on the 2-category of groupoids. Action containers are endowed with groups that act on their positions, with morphisms preserving the actions. We show that, as a category, action containers are equivalent to the free coproduct completion of a category of group actions. We derive that they model non-inductive single-variable strictly positive types in the sense of Abbott et al.: The category of action containers is closed under arbitrary (co)products and exponentiation with constants. We equip this category with the structure of a locally groupoidal 2-category, and prove that it locally embeds into the 2-category of symmetric containers. This follows from the embedding of a 2-category of groups into the 2-category of groupoids, extending the delooping construction.
Cite as

Philipp Joram and Niccolò Veltri. Data Types with Symmetries via Action Containers. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{joram_et_al:LIPIcs.TYPES.2024.6,
  author =	{Joram, Philipp and Veltri, Niccol\`{o}},
  title =	{{Data Types with Symmetries via Action Containers}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{6:1--6:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers 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.2024.6},
  URN =		{urn:nbn:de:0030-drops-233681},
  doi =		{10.4230/LIPIcs.TYPES.2024.6},
  annote =	{Keywords: Containers, Homotopy Type Theory, Agda, 2-categories}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.40
Completeness of First-Order Bi-Intuitionistic Logic

Authors: Dominik Kirst and Ian Shillito

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
We provide a succinct and verified completeness proof for first-order bi-intuitionistic logic, relative to constant domain Kripke semantics. By doing so, we make up for the almost-50-year-old substantial mistakes in Rauszer’s foundational work, detected but unresolved by Shillito two years ago. Moreover, an even earlier but historically neglected proof by Klemke has been found to contain at least local errors by Olkhovikov and Badia, that remained unfixed due to the technical complexity of Klemke’s argument. To resolve this unclear situation once and for all, we give a succinct completeness proof, based on and dualising a standard proof for constant domain intuitionistic logic, and verify our constructions using the Coq proof assistant to guarantee correctness.
Cite as

Dominik Kirst and Ian Shillito. Completeness of First-Order Bi-Intuitionistic Logic. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 40:1-40:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kirst_et_al:LIPIcs.CSL.2025.40,
  author =	{Kirst, Dominik and Shillito, Ian},
  title =	{{Completeness of First-Order Bi-Intuitionistic Logic}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{40:1--40:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.40},
  URN =		{urn:nbn:de:0030-drops-227979},
  doi =		{10.4230/LIPIcs.CSL.2025.40},
  annote =	{Keywords: bi-intuitionistic logic, first-order logic, completeness, Coq proof assistant}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.26
A Formal Proof of Modal Completeness for Provability Logic

Authors: Marco Maggesi and Cosimo Perini Brogi

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

Abstract
This work presents a formalized proof of modal completeness for Gödel-Löb provability logic (GL) in the HOL Light theorem prover. We describe the code we developed, and discuss some details of our implementation. In particular, we show how we adapted the proof in the Boolos' monograph according to the formal language and tools at hand. The strategy we develop here overcomes the technical difficulty due to the non-compactness of GL, and simplify the implementation. Moreover, it can be applied to other normal modal systems with minimal changes.
Cite as

Marco Maggesi and Cosimo Perini Brogi. A Formal Proof of Modal Completeness for Provability Logic. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{maggesi_et_al:LIPIcs.ITP.2021.26,
  author =	{Maggesi, Marco and Perini Brogi, Cosimo},
  title =	{{A Formal Proof of Modal Completeness for Provability Logic}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{26:1--26:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.26},
  URN =		{urn:nbn:de:0030-drops-139215},
  doi =		{10.4230/LIPIcs.ITP.2021.26},
  annote =	{Keywords: Provability Logic, Higher-Order Logic, Mechanized Mathematics, HOL Light Theorem Prover}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.5
Bicategories in Univalent Foundations

Authors: Benedikt Ahrens, Dan Frumin, Marco Maggesi, and Niels van der Weide

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of those, we develop the notion of "displayed bicategories", an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. Displayed bicategories allow us to construct univalent bicategories in a modular fashion. To demonstrate the applicability of this notion, we prove several bicategories are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Our work is formalized in the UniMath library of univalent mathematics.
Cite as

Benedikt Ahrens, Dan Frumin, Marco Maggesi, and Niels van der Weide. Bicategories in Univalent Foundations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.FSCD.2019.5,
  author =	{Ahrens, Benedikt and Frumin, Dan and Maggesi, Marco and van der Weide, Niels},
  title =	{{Bicategories in Univalent Foundations}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.5},
  URN =		{urn:nbn:de:0030-drops-105124},
  doi =		{10.4230/LIPIcs.FSCD.2019.5},
  annote =	{Keywords: bicategory theory, univalent mathematics, dependent type theory, Coq}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.6
Modular Specification of Monads Through Higher-Order Presentations

Authors: Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they associate a category of "models", and they give a monadicity result which implies that this category has an initial object, which is the language presented by the pair. In the present work, we propose, for the untyped setting, a variant of their approach where monads and modules over them are the central notions. More precisely, we study, for monads over sets, presentations by generating ("higher-order") operations and equations among them. We consider a notion of 2-signature which allows to specify a monad with a family of binding operations subject to a family of equations, as is the case for the paradigmatic example of the lambda calculus, specified by its two standard constructions (application and abstraction) subject to beta- and eta-equalities. Such a 2-signature is hence a pair (Sigma,E) of a binding signature Sigma and a family E of equations for Sigma. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context. We associate, to each 2-signature (Sigma,E), a category of "models of (Sigma,E)"; and we say that a 2-signature is "effective" if this category has an initial object; the monad underlying this (essentially unique) object is the "monad specified by the 2-signature". Not every 2-signature is effective; we identify a class of 2-signatures, which we call "algebraic", that are effective. Importantly, our 2-signatures together with their models enjoy "modularity": when we glue (algebraic) 2-signatures together, their initial models are glued accordingly. We provide a computer formalization for our main results.
Cite as

Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. Modular Specification of Monads Through Higher-Order Presentations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.FSCD.2019.6,
  author =	{Ahrens, Benedikt and Hirschowitz, Andr\'{e} and Lafont, Ambroise and Maggesi, Marco},
  title =	{{Modular Specification of Monads Through Higher-Order Presentations}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{6:1--6:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.6},
  URN =		{urn:nbn:de:0030-drops-105136},
  doi =		{10.4230/LIPIcs.FSCD.2019.6},
  annote =	{Keywords: free monads, presentation of monads, initial semantics, signatures, syntax, monadic substitution, computer-checked proofs}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.4
High-Level Signatures and Initial Semantics

Authors: Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
We present a device for specifying and reasoning about syntax for datatypes, programming languages, and logic calculi. More precisely, we consider a general notion of "signature" for specifying syntactic constructions. Our signatures subsume classical algebraic signatures (i.e., signatures for languages with variable binding, such as the pure lambda calculus) and extend to much more general examples. In the spirit of Initial Semantics, we define the "syntax generated by a signature" to be the initial object - if it exists - in a suitable category of models. Our notions of signature and syntax are suited for compositionality and provide, beyond the desired algebra of terms, a well-behaved substitution and the associated inductive/recursive principles. Our signatures are "general" in the sense that the existence of an associated syntax is not automatically guaranteed. In this work, we identify a large and simple class of signatures which do generate a syntax. This paper builds upon ideas from a previous attempt by Hirschowitz-Maggesi, which, in turn, was directly inspired by some earlier work of Ghani-Uustalu-Hamana and Matthes-Uustalu. The main results presented in the paper are computer-checked within the UniMath system.
Cite as

Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. High-Level Signatures and Initial Semantics. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 4:1-4:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.CSL.2018.4,
  author =	{Ahrens, Benedikt and Hirschowitz, Andr\'{e} and Lafont, Ambroise and Maggesi, Marco},
  title =	{{High-Level Signatures and Initial Semantics}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{4:1--4:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.4},
  URN =		{urn:nbn:de:0030-drops-96713},
  doi =		{10.4230/LIPIcs.CSL.2018.4},
  annote =	{Keywords: initial semantics, signatures, syntax, monadic substitution, computer-checked proofs}
}
  • Refine by Type
  • 8 Document/PDF
  • 4 Document/HTML
  • 2 Artifact

  • Refine by Publication Year
  • 3 2026
  • 3 2025
  • 1 2021
  • 2 2019
  • 1 2018

  • Refine by Author
  • 7 Maggesi, Marco
  • 4 Ahrens, Benedikt
  • 4 Perini Brogi, Cosimo
  • 3 Bilotta, Antonella
  • 2 Hirschowitz, André
  • Show More...

  • Refine by Series/Journal
  • 8 LIPIcs

  • Refine by Classification
  • 3 Theory of computation → Logic and verification
  • 3 Theory of computation → Modal and temporal logics
  • 3 Theory of computation → Type theory
  • 2 Theory of computation → Algebraic language theory
  • 2 Theory of computation → Automated reasoning
  • Show More...

  • Refine by Keyword
  • 3 HOL Light
  • 2 Automated Reasoning
  • 2 Modal Logic
  • 2 Proof Assistants
  • 2 Theorem Proving
  • 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-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact