Issue
Dagstuhl Reports, Volume 14, Issue 1
-
Part of:
Volume:
Dagstuhl Reports, Volume 14
Journal: Dagstuhl Reports (DagRep)
Event
Dagstuhl Seminars 24021, 24031, 24032, 24041, 24042, 24051, 24052Publication Details
- published at: 2024-07-30
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Complete Issue
Dagstuhl Reports, Volume 14, Issue 1, January 2024, Complete Issue
Abstract
Dagstuhl Reports, Volume 14, Issue 1, January 2024, Complete Issue
Cite as
Dagstuhl Reports, Volume 14, Issue 1, pp. 1-163, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{DagRep.14.1,
title = {{Dagstuhl Reports, Volume 14, Issue 1, January 2024, Complete Issue}},
pages = {1--163},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2024},
volume = {14},
number = {1},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1},
URN = {urn:nbn:de:0030-drops-204861},
doi = {10.4230/DagRep.14.1},
annote = {Keywords: Dagstuhl Reports, Volume 14, Issue 1, January 2024, Complete Issue}
}
Document
Front Matter
Dagstuhl Reports, Table of Contents, Volume 14, Issue 1, 2024
Abstract
Dagstuhl Reports, Table of Contents, Volume 14, Issue 1, 2024
Cite as
Dagstuhl Reports, Volume 14, Issue 1, pp. i-ii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{DagRep.14.1.i,
title = {{Dagstuhl Reports, Table of Contents, Volume 14, Issue 1, 2024}},
pages = {i--ii},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2024},
volume = {14},
number = {1},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.i},
URN = {urn:nbn:de:0030-drops-204874},
doi = {10.4230/DagRep.14.1.i},
annote = {Keywords: Table of Contents, Frontmatter}
}
Document
From Proofs to Computation in Geometric Logic and Generalizations (Dagstuhl Seminar 24021)
Abstract
What is the computational content of proofs? This is one of the main topics in mathematical logic, especially proof theory, that is of relevance for computer science. The well-known foundational solutions aim at rebuilding mathematics constructively almost from scratch, and include Bishop-style constructive mathematics and Martin-Löf’s intuitionistic type theory, the latter most recently in the form of the so-called homotopy or univalent type theory put forward by Voevodsky.
From a more practical angle, however, the question rather is to which extent any given proof is effective, which proofs of which theorems can be rendered effective, and whether and how numerical information such as bounds and algorithms can be extracted from proofs. Ideally, all this is done by manipulating proofs mechanically and/or by adequate metatheorems (proof translations, automated theorem proving, program extraction from proofs, proof mining, etc.).
A crucial role for answering these questions is played by coherent and geometric theories and their generalizations: not only that they are fairly widespread in modern mathematics and non-classical logics (e.g., in abstract algebra, and in temporal and modal logics); those theories are also a priori amenable for constructivisation (see Barr’s Theorem, especially its proof-theoretic variants, and the numerous Glivenko–style theorems); last but not least, effective theorem-proving for coherent theories can be automated with relative ease and clarity in relation to resolution.
Specific topics that substantially involve computer science research include categorical semantics for geometric theories up to the proof-theoretic presentation of sheaf models and higher toposes; extracting the computational content of proofs and dynamical methods in quadratic form theory; the interpretation of transfinite proof methods as latent computations; complexity issues of and algorithms for geometrization of theories; the use of geometric theories in constructive mathematics including finding algorithms, ideally with integrated developments; and coherent logic for obtaining automatically readable proofs.
Cite as
Ingo Blechschmidt, Hajime Ishihara, Peter M. Schuster, and Gabriele Buriola. From Proofs to Computation in Geometric Logic and Generalizations (Dagstuhl Seminar 24021). In Dagstuhl Reports, Volume 14, Issue 1, pp. 1-24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{blechschmidt_et_al:DagRep.14.1.1,
author = {Blechschmidt, Ingo and Ishihara, Hajime and Schuster, Peter M. and Buriola, Gabriele},
title = {{From Proofs to Computation in Geometric Logic and Generalizations (Dagstuhl Seminar 24021)}},
pages = {1--24},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2024},
volume = {14},
number = {1},
editor = {Blechschmidt, Ingo and Ishihara, Hajime and Schuster, Peter M. and Buriola, Gabriele},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.1},
URN = {urn:nbn:de:0030-drops-204882},
doi = {10.4230/DagRep.14.1.1},
annote = {Keywords: automated theorem proving, categorical semantics, constructivisation, geometric logic, proof theory}
}
Document
Fusing Causality, Reasoning, and Learning for Fault Management and Diagnosis (Dagstuhl Seminar 24031)
Abstract
This report documents the program and the outcomes of Dagstuhl Seminar "Fusing Causality, Reasoning, and Learning for Fault Management and Diagnosis" (24031). The goal of this Dagstuhl Seminar was to provide an interdisciplinary forum to discuss the fundamental principles of fault management and diagnosis, bringing together international researchers and practitioners from the fields of symbolic reasoning, machine learning, and control engineering.
Cite as
Alessandro Cimatti, Ingo Pill, and Alexander Diedrich. Fusing Causality, Reasoning, and Learning for Fault Management and Diagnosis (Dagstuhl Seminar 24031). In Dagstuhl Reports, Volume 14, Issue 1, pp. 25-48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{cimatti_et_al:DagRep.14.1.25,
author = {Cimatti, Alessandro and Pill, Ingo and Diedrich, Alexander},
title = {{Fusing Causality, Reasoning, and Learning for Fault Management and Diagnosis (Dagstuhl Seminar 24031)}},
pages = {25--48},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2024},
volume = {14},
number = {1},
editor = {Cimatti, Alessandro and Pill, Ingo and Diedrich, Alexander},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.25},
URN = {urn:nbn:de:0030-drops-204899},
doi = {10.4230/DagRep.14.1.25},
annote = {Keywords: cyber-physical systems, diagnosis, fault detection and management, integrative ai, model-based reasoning}
}
Document
Representation, Provenance, and Explanations in Database Theory and Logic (Dagstuhl Seminar 24032)
Abstract
This report documents the program and the outcomes of Dagstuhl Seminar "Representation, Provenance, and Explanations in Database Theory and Logic" (24032), which was broadly in the area of database theory. Database theory formalizes the theoretical underpinnings of databases and analyzes them with mathematical tools. We focused on questions related to the fundamental problem of efficient query evaluation: compute the answers of a query on a database. This seminar focused on three key aspects of query evaluations. (1) Representation studies the tradeoff between expressivity, compactness, and efficient computation of outputs from the inputs, including circuits and knowledge compilation forms, enumeration, and direct access. (2) Provenance captures the computation process of outputs from the inputs using a compact formula, and has applications to probabilistic databases. (3) Explanations give meaningful insights to responsibilities of different inputs toward an output beyond provenance, e.g., by using Shapley Values from co-operative game theory that has been recently popular in both DB and ML.
Cite as
Pablo Barcelo, Pierre Bourhis, Stefan Mengel, and Sudeepa Roy. Representation, Provenance, and Explanations in Database Theory and Logic (Dagstuhl Seminar 24032). In Dagstuhl Reports, Volume 14, Issue 1, pp. 49-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{barcelo_et_al:DagRep.14.1.49,
author = {Barcelo, Pablo and Bourhis, Pierre and Mengel, Stefan and Roy, Sudeepa},
title = {{Representation, Provenance, and Explanations in Database Theory and Logic (Dagstuhl Seminar 24032)}},
pages = {49--71},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2024},
volume = {14},
number = {1},
editor = {Barcelo, Pablo and Bourhis, Pierre and Mengel, Stefan and Roy, Sudeepa},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.49},
URN = {urn:nbn:de:0030-drops-204904},
doi = {10.4230/DagRep.14.1.49},
annote = {Keywords: Circuits, database theory, factorized databases, provenance, shapley values}
}
Document
Symmetric Cryptography (Dagstuhl Seminar 24041)
Abstract
This report documents the program and the outcomes of Dagstuhl Seminar "Symmetric Cryptography" (24041). The seminar was held on January 21-26, 2024 in Schloss Dagstuhl - Leibniz Center for Informatics. This was the ninth seminar in the series "Symmetric Cryptography". Previous editions were held in 2007, 2009, 2012, 2014, 2016, 2018, 2020 and 2022. Participants of the seminar presented their ongoing work and new results on topics of cryptanalysis and (post-quantum) provable security of symmetric cryptographic primitives. Participants also worked together within seven research group dedicated to various topics (Cryptanalysis of Poseidon, Cryptanalysis of TEA-3, Exploitation of the wrong key randomization hypothesis non-conformity in key recovery attacks, Cryptanalysis of SCARF, Differential cryptanalysis and more, Key control security and Security of sponge combiners). In this report, a brief summary of the seminar is given, followed by the abstracts of given talks and a summary of the progress of each research group.
Cite as
Christof Beierle, Bart Mennink, María Naya-Plasencia, Yu Sasaki, and Rachelle Heim Boissier. Symmetric Cryptography (Dagstuhl Seminar 24041). In Dagstuhl Reports, Volume 14, Issue 1, pp. 72-89, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{beierle_et_al:DagRep.14.1.72,
author = {Beierle, Christof and Mennink, Bart and Naya-Plasencia, Mar{\'\i}a and Sasaki, Yu and Boissier, Rachelle Heim},
title = {{Symmetric Cryptography (Dagstuhl Seminar 24041)}},
pages = {72--89},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2024},
volume = {14},
number = {1},
editor = {Beierle, Christof and Mennink, Bart and Naya-Plasencia, Mar{\'\i}a and Sasaki, Yu and Boissier, Rachelle Heim},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.72},
URN = {urn:nbn:de:0030-drops-204915},
doi = {10.4230/DagRep.14.1.72},
annote = {Keywords: Lightweight Cryptography, New Applications of Symmetric Cryptography, Permutation-Based Cryptography}
}
Document
The Emerging Issues in Bioimaging AI Publications and Research (Dagstuhl Seminar 24042)
Abstract
This report documents the program and outcomes of Dagstuhl Seminar "The Emerging Issues in Bioimaging AI Publications and Research" (24042) held on January 21-24, 2024. The fast advancement of computational techniques, particularly those based on artificial intelligence (AI), has significantly propelled the field of computational biology. With the rapid development, new issues are emerging in bioimaging AI publications and research. For example, how can we properly validate the AI methods used in quantitative biological analysis? Also, the ethical aspects of these developments remain underexplored, lacking clear definitions and recognition within the community. The goal of this interdisciplinary seminar was to bring together experts from various fields, including experimental biology, computational biology, bioimage analysis, computer vision, and AI research, to identify, discuss and address the emerging issues in current bioimaging AI research and publications.
Cite as
Jianxu Chen, Florian Jug, Susanne Rafelski, and Shanghang Zhang. The Emerging Issues in Bioimaging AI Publications and Research (Dagstuhl Seminar 24042). In Dagstuhl Reports, Volume 14, Issue 1, pp. 90-107, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{chen_et_al:DagRep.14.1.90,
author = {Chen, Jianxu and Jug, Florian and Rafelski, Susanne and Zhang, Shanghang},
title = {{The Emerging Issues in Bioimaging AI Publications and Research (Dagstuhl Seminar 24042)}},
pages = {90--107},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2024},
volume = {14},
number = {1},
editor = {Chen, Jianxu and Jug, Florian and Rafelski, Susanne and Zhang, Shanghang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.90},
URN = {urn:nbn:de:0030-drops-204928},
doi = {10.4230/DagRep.14.1.90},
annote = {Keywords: artificial intelligence, bioimaging, open source, publication ethics, trustworthy ai}
}
Document
Next Generation Protocols for Heterogeneous Systems (Dagstuhl Seminar 24051)
Abstract
The emergence of new computing systems, like cloud computing, blockchains, and Internet of Things (IoT), replaces the traditional monolithic software hardware stack with a distributed heterogeneous model. This change poses new demands on the programming languages for developing such systems: compositionality, allowing decomposition of a system into smaller, possibly heterogeneous, parts and composition of the individually verified parts into a verified whole, security, asserting end-to-end integrity and confidentiality, quantitative reasoning methods, accounting for timing and probabilistic events, and, as a cross-cutting concern, certification of asserted properties in terms of independently verifiable, machine-checked proofs.
Characteristics of this emerging computation model are distribution of the participating entities and message passing as the primary means of communication. Message passing is also the communication model underlying behavioral types and programming languages, making them uniquely fitted for this new application domain. Behavioral types explicitly capture the protocols of message exchange and have a strong theoretical foundation. Recent applications of behavioral types include smart contract languages, information flow control, and machine-checked proofs of safety properties. Although these early explorations are promising, the current state of the art of behavioral types and programming languages lacks a comprehensive account of the above-mentioned demands.
This Dagstuhl Seminar aims to gather experts from academia and industry to discuss the use of programming languages tailored to tackle the challenges posed by today’s emerging distributed and heterogeneous computing platforms, e.g., by making use of behavioral types. It will focus on static and possibly dynamic mechanisms to support compositionality, security, quantitative reasoning, and certification.
Cite as
Stephanie Balzer, Marco Carbone, Roland Kuhn, and Peter Thiemann. Next Generation Protocols for Heterogeneous Systems (Dagstuhl Seminar 24051). In Dagstuhl Reports, Volume 14, Issue 1, pp. 108-129, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{balzer_et_al:DagRep.14.1.108,
author = {Balzer, Stephanie and Carbone, Marco and Kuhn, Roland and Thiemann, Peter},
title = {{Next Generation Protocols for Heterogeneous Systems (Dagstuhl Seminar 24051)}},
pages = {108--129},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2024},
volume = {14},
number = {1},
editor = {Balzer, Stephanie and Carbone, Marco and Kuhn, Roland and Thiemann, Peter},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.108},
URN = {urn:nbn:de:0030-drops-204930},
doi = {10.4230/DagRep.14.1.108},
annote = {Keywords: behavioural types, concurrency, programming languages, session types}
}
Document
Reviewer No. 2: Old and New Problems in Peer Review (Dagstuhl Seminar 24052)
Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 24052 "Reviewer No. 2: Old and New Problems in Peer Review". This seminar provided a point of reflection on decades of personal experience of the participants in organizing different kinds of peer-reviewed venues in Natural Language Processing (NLP) and beyond, enabling an in-depth discussion of what has been tried, what seems to work and what doesn't. The outcomes of the seminar include a white paper co-authored by most of the seminar participants, which outlines the research program, methodological and empirical challenges for NLP for peer review. The discussions at the seminar also resulted in several concrete policy proposals and initiatives, some of which are already in motion at the Association for Computational Linguistics and elsewhere.
Cite as
Iryna Gurevych, Anna Rogers, Nihar B. Shah, and Jingyan Wang. Reviewer No. 2: Old and New Problems in Peer Review (Dagstuhl Seminar 24052). In Dagstuhl Reports, Volume 14, Issue 1, pp. 130-161, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{gurevych_et_al:DagRep.14.1.130,
author = {Gurevych, Iryna and Rogers, Anna and Shah, Nihar B. and Wang, Jingyan},
title = {{Reviewer No. 2: Old and New Problems in Peer Review (Dagstuhl Seminar 24052)}},
pages = {130--161},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2024},
volume = {14},
number = {1},
editor = {Gurevych, Iryna and Rogers, Anna and Shah, Nihar B. and Wang, Jingyan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.130},
URN = {urn:nbn:de:0030-drops-204941},
doi = {10.4230/DagRep.14.1.130},
annote = {Keywords: Peer Review, Natural Language Processing}
}