Issue
Dagstuhl Reports, Volume 14, Issue 8
-
Part of:
Volume:
Dagstuhl Reports, Volume 14
Journal: Dagstuhl Reports (DagRep)
Event
Dagstuhl Seminars 24341, 24342, 24351, 24352 (Perspectives Workshop)Publication Details
- published at: 2025-03-13
- 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 8, August 2024, Complete Issue
Abstract
Dagstuhl Reports, Volume 14, Issue 8, August 2024, Complete Issue
Cite as
Dagstuhl Reports, Volume 14, Issue 8, pp. 1-60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{DagRep.14.8,
title = {{Dagstuhl Reports, Volume 14, Issue 8, August 2024, Complete Issue}},
pages = {1--60},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2025},
volume = {14},
number = {8},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.8},
URN = {urn:nbn:de:0030-drops-229984},
doi = {10.4230/DagRep.14.8},
annote = {Keywords: Dagstuhl Reports, Volume 14, Issue 8, August 2024, Complete Issue}
}
Document
Front Matter
Dagstuhl Reports, Table of Contents, Volume 14, Issue 8, 2024
Abstract
Dagstuhl Reports, Table of Contents, Volume 14, Issue 8, 2024
Cite as
Dagstuhl Reports, Volume 14, Issue 8, pp. i-ii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{DagRep.14.8.i,
title = {{Dagstuhl Reports, Table of Contents, Volume 14, Issue 8, 2024}},
pages = {i--ii},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2025},
volume = {14},
number = {8},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.8.i},
URN = {urn:nbn:de:0030-drops-229934},
doi = {10.4230/DagRep.14.8.i},
annote = {Keywords: Table of Contents, Frontmatter}
}
Document
Proof Representations: From Theory to Applications (Dagstuhl Seminar 24341)
Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 24341 "Proof Representations: From Theory to Applications". Proof theory is the study of formal proofs as mathematical objects in their own right. The subject has enjoyed continued attention among computer scientists in particular due to its significance for formalization, metalogic, and automation. In recent decades there has been a surge of interest on the representations of formal proofs themselves. The outcomes of these investigations have been remarkable, in particular extending the scope of structural proof theory to novel and richer settings:
Richer line structures (e.g. hypersequents, nested sequents, labelled sequents) have resulted in a uniform treatment of standard modal logics, streamlining their metatheory and providing new tools for metalogical problems. Richer proof structures (e.g., cyclic proofs, annotated systems, infinitely branching proofs) have significantly advanced our understanding of fixed points and (co)induction. Indeed, we are now seeing many of these previously disjoint techniques being combined to push the boundaries of proof theoretic approaches to computational logic. Graphical proof representations (e.g., proof nets, atomic flows, combinatorial proofs) originating from "linear" logics, now not only comprise a well-behaved computational model for resource-sensitive reasoning, but also provide an impressively uniform treatment for logics across the board. In fact, we are now seeing many of these previously disjoint techniques being combined to push the boundaries of proof theoretic approaches to computational logic, which has produced deep and fruitful cross-fertilizations between programming languages and proof theory. Arguably, the most well-known is the Curry-Howard correspondence ("propositions-as-types") where (functional) programs correspond to formal proofs and their execution to normalization. A complementary tradition, proof-search-as-computation ("propositions-as-processes"), instead interprets (logic) programs to formulas and their execution to proof search.
The goal of this Dagstuhl Seminar was twofold. First and foremost, we aimed to bring together theorists and practitioners exploiting proof representations to identify new directions of application and, simultaneously, distill new theoretical directions from problems "in the wild". At the same time, this seminar was intended to expose the interface between the proof-normalization and proof-search traditions by probing proof representations from both directions.
Cite as
Anupam Das, Elaine Pimentel, Lutz Straßburger, and Robin Martinot. Proof Representations: From Theory to Applications (Dagstuhl Seminar 24341). In Dagstuhl Reports, Volume 14, Issue 8, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{das_et_al:DagRep.14.8.1,
author = {Das, Anupam and Pimentel, Elaine and Stra{\ss}burger, Lutz and Martinot, Robin},
title = {{Proof Representations: From Theory to Applications (Dagstuhl Seminar 24341)}},
pages = {1--23},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2025},
volume = {14},
number = {8},
editor = {Das, Anupam and Pimentel, Elaine and Stra{\ss}burger, Lutz and Martinot, Robin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.8.1},
URN = {urn:nbn:de:0030-drops-229975},
doi = {10.4230/DagRep.14.8.1},
annote = {Keywords: proof theory, proof calculi, computational interpretations, proof semantics, dynamic operators}
}
Document
Leveraging AI for Management Decision-Making (Dagstuhl Seminar 24342)
Abstract
Artificial intelligence (AI) is transforming decision-making across industries and management functions, which leads to increased operational efficiency and creates significant economic impact. A recent surge in attention to AI in business decision-making has been driven by new AI technologies - such as deep learning, causal machine learning, generative AI and explainable AI - and their applications in areas like operations, marketing, information systems, and quality management. Yet, the potential of AI to optimize business decisions also introduces ethical, legal, and societal challenges, particularly in high-stakes business settings. This motivates our Dagstuhl Seminar, which aimed to foster interdisciplinary collaboration between scholars in management and computer science, as well as practitioners from industry. As a result, the seminar generated new suggestions for the field to evolve in the future by identifying new research opportunities with managerial relevance.
Cite as
Stefan Feuerriegel, Foster Provost, and Galit Shmueli. Leveraging AI for Management Decision-Making (Dagstuhl Seminar 24342). In Dagstuhl Reports, Volume 14, Issue 8, pp. 24-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{feuerriegel_et_al:DagRep.14.8.24,
author = {Feuerriegel, Stefan and Provost, Foster and Shmueli, Galit},
title = {{Leveraging AI for Management Decision-Making (Dagstuhl Seminar 24342)}},
pages = {24--35},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2025},
volume = {14},
number = {8},
editor = {Feuerriegel, Stefan and Provost, Foster and Shmueli, Galit},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.8.24},
URN = {urn:nbn:de:0030-drops-229961},
doi = {10.4230/DagRep.14.8.24},
annote = {Keywords: applications, business, decision-making, management, marketing}
}
Document
Power, Energy, and Carbon-Aware Computing on Heterogeneous Systems (PEACHES) (Dagstuhl Seminar 24351)
Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 24351 "Power, Energy, and Carbon-Aware Computing on Heterogeneous Systems (PEACHES)".
Cite as
Kerstin I. Eder, Timo Hönig, Maja Hanne Kirkeby, Daniel Mosse, Max Plauth, and Jonas Juffinger. Power, Energy, and Carbon-Aware Computing on Heterogeneous Systems (PEACHES) (Dagstuhl Seminar 24351). In Dagstuhl Reports, Volume 14, Issue 8, pp. 36-52, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{eder_et_al:DagRep.14.8.36,
author = {Eder, Kerstin I. and H\"{o}nig, Timo and Kirkeby, Maja Hanne and Mosse, Daniel and Plauth, Max and Juffinger, Jonas},
title = {{Power, Energy, and Carbon-Aware Computing on Heterogeneous Systems (PEACHES) (Dagstuhl Seminar 24351)}},
pages = {36--52},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2025},
volume = {14},
number = {8},
editor = {Eder, Kerstin I. and H\"{o}nig, Timo and Kirkeby, Maja Hanne and Mosse, Daniel and Plauth, Max and Juffinger, Jonas},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.8.36},
URN = {urn:nbn:de:0030-drops-229958},
doi = {10.4230/DagRep.14.8.36},
annote = {Keywords: Carbon, Energy, Operating Systems, Power, Ressource Efficiency, Systems}
}
Document
Conversational Agents: A Framework for Evaluation (CAFE) (Dagstuhl Perspectives Workshop 24352)
Abstract
This report documents the program and the outcomes of the Dagstuhl Perspectives Workshop 24352, "Conversational Agents: A Framework for Evaluation (CAFE)", which brought together 22 distinguished researchers and practitioners from 12 countries. In this workshop, a new framework for the evaluation of conversational information access systems was developed, consisting of six major components: 1) goals of the system’s stakeholders, 2) user tasks to be studied in the evaluation, 3) aspects of the users carrying out the tasks, 4) evaluation criteria to be considered, 5) evaluation methodology to be applied, and 6) measures for the quantitative criteria chosen. An evaluation design begins with identifying the stakeholders, whose goals determine the criteria. Tasks and evaluation methodology should be chosen according to these decisions.
Cite as
Christine Bauer, Li Chen, Nicola Ferro, and Norbert Fuhr. Conversational Agents: A Framework for Evaluation (CAFE) (Dagstuhl Perspectives Workshop 24352). In Dagstuhl Reports, Volume 14, Issue 8, pp. 53-58, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
Copy BibTex To Clipboard
@Article{bauer_et_al:DagRep.14.8.53,
author = {Bauer, Christine and Chen, Li and Ferro, Nicola and Fuhr, Norbert},
title = {{Conversational Agents: A Framework for Evaluation (CAFE) (Dagstuhl Perspectives Workshop 24352)}},
pages = {53--58},
journal = {Dagstuhl Reports},
ISSN = {2192-5283},
year = {2025},
volume = {14},
number = {8},
editor = {Bauer, Christine and Chen, Li and Ferro, Nicola and Fuhr, Norbert},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.8.53},
URN = {urn:nbn:de:0030-drops-229940},
doi = {10.4230/DagRep.14.8.53},
annote = {Keywords: Conversational Agents, Evaluation, Information Access, Dagstuhl Perspectives Workshop}
}