Published in: Dagstuhl Manifestos, Volume 11, Issue 1 (2025)
Christine Bauer, Li Chen, Nicola Ferro, Norbert Fuhr, Avishek Anand, Timo Breuer, Guglielmo Faggioli, Ophir Frieder, Hideo Joho, Jussi Karlgren, Johannes Kiesel, Bart P. Knijnenburg, Aldo Lipani, Lien Michiels, Andrea Papenmeier, Maria Soledad Pera, Mark Sanderson, Scott Sanner, Benno Stein, Johanne R. Trippas, Karin Verspoor, and Martijn C. Willemsen. Conversational Agents: A Framework for Evaluation (CAFE) (Dagstuhl Perspectives Workshop 24352). In Dagstuhl Manifestos, Volume 11, Issue 1, pp. 19-67, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@Article{bauer_et_al:DagMan.11.1.19,
author = {Bauer, Christine and Chen, Li and Ferro, Nicola and Fuhr, Norbert and Anand, Avishek and Breuer, Timo and Faggioli, Guglielmo and Frieder, Ophir and Joho, Hideo and Karlgren, Jussi and Kiesel, Johannes and Knijnenburg, Bart P. and Lipani, Aldo and Michiels, Lien and Papenmeier, Andrea and Pera, Maria Soledad and Sanderson, Mark and Sanner, Scott and Stein, Benno and Trippas, Johanne R. and Verspoor, Karin and Willemsen, Martijn C.},
title = {{Conversational Agents: A Framework for Evaluation (CAFE) (Dagstuhl Perspectives Workshop 24352)}},
pages = {19--67},
journal = {Dagstuhl Manifestos},
ISSN = {2193-2433},
year = {2025},
volume = {11},
number = {1},
editor = {Bauer, Christine and Chen, Li and Ferro, Nicola and Fuhr, Norbert and Anand, Avishek and Breuer, Timo and Faggioli, Guglielmo and Frieder, Ophir and Joho, Hideo and Karlgren, Jussi and Kiesel, Johannes and Knijnenburg, Bart P. and Lipani, Aldo and Michiels, Lien and Papenmeier, Andrea and Pera, Maria Soledad and Sanderson, Mark and Sanner, Scott and Stein, Benno and Trippas, Johanne R. and Verspoor, Karin and Willemsen, Martijn C.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagMan.11.1.19},
URN = {urn:nbn:de:0030-drops-252722},
doi = {10.4230/DagMan.11.1.19},
annote = {Keywords: Conversational Agents, Evaluation, Information Access}
}
Published in: TGDK, Volume 3, Issue 2 (2025). Transactions on Graph Data and Knowledge, Volume 3, Issue 2
Arnab Sharma, N'Dah Jean Kouagou, and Axel-Cyrille Ngonga Ngomo. Resilience in Knowledge Graph Embeddings. In Transactions on Graph Data and Knowledge (TGDK), Volume 3, Issue 2, pp. 1:1-1:38, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@Article{sharma_et_al:TGDK.3.2.1,
author = {Sharma, Arnab and Kouagou, N'Dah Jean and Ngomo, Axel-Cyrille Ngonga},
title = {{Resilience in Knowledge Graph Embeddings}},
journal = {Transactions on Graph Data and Knowledge},
pages = {1:1--1:38},
ISSN = {2942-7517},
year = {2025},
volume = {3},
number = {2},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/TGDK.3.2.1},
URN = {urn:nbn:de:0030-drops-248117},
doi = {10.4230/TGDK.3.2.1},
annote = {Keywords: Knowledge graphs, Resilience, Robustness}
}
Published in: TGDK, Volume 3, Issue 2 (2025). Transactions on Graph Data and Knowledge, Volume 3, Issue 2
Henri Scaffidi, Melinda Hodkiewicz, Caitlin Woods, and Nicole Roocke. GraphRAG on Technical Documents - Impact of Knowledge Graph Schema. In Transactions on Graph Data and Knowledge (TGDK), Volume 3, Issue 2, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@Article{scaffidi_et_al:TGDK.3.2.3,
author = {Scaffidi, Henri and Hodkiewicz, Melinda and Woods, Caitlin and Roocke, Nicole},
title = {{GraphRAG on Technical Documents - Impact of Knowledge Graph Schema}},
journal = {Transactions on Graph Data and Knowledge},
pages = {3:1--3:24},
ISSN = {2942-7517},
year = {2025},
volume = {3},
number = {2},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/TGDK.3.2.3},
URN = {urn:nbn:de:0030-drops-248131},
doi = {10.4230/TGDK.3.2.3},
annote = {Keywords: RAG, minerals, local search, global search, entity extraction, competency questions}
}
Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)
Monika Henzinger and Roodabeh Safavi. Securing Dynamic Data: A Primer on Differentially Private Data Structures (Invited Talk). In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{henzinger_et_al:LIPIcs.ESA.2025.2,
author = {Henzinger, Monika and Safavi, Roodabeh},
title = {{Securing Dynamic Data: A Primer on Differentially Private Data Structures}},
booktitle = {33rd Annual European Symposium on Algorithms (ESA 2025)},
pages = {2:1--2:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-395-9},
ISSN = {1868-8969},
year = {2025},
volume = {351},
editor = {Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.2},
URN = {urn:nbn:de:0030-drops-244702},
doi = {10.4230/LIPIcs.ESA.2025.2},
annote = {Keywords: Differential privacy, continual observation}
}
Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)
Bingbing Hu and Adam Polak. Non-Boolean OMv: One More Reason to Believe Lower Bounds for Dynamic Problems. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 54:1-54:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{hu_et_al:LIPIcs.ESA.2025.54,
author = {Hu, Bingbing and Polak, Adam},
title = {{Non-Boolean OMv: One More Reason to Believe Lower Bounds for Dynamic Problems}},
booktitle = {33rd Annual European Symposium on Algorithms (ESA 2025)},
pages = {54:1--54:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-395-9},
ISSN = {1868-8969},
year = {2025},
volume = {351},
editor = {Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.54},
URN = {urn:nbn:de:0030-drops-245228},
doi = {10.4230/LIPIcs.ESA.2025.54},
annote = {Keywords: Fine-grained complexity, OMv hypothesis, reductions, equivalence class}
}
Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)
Francisco Sena, Romeo Rizzi, and Alexandru I. Tomescu. Safe Sequences via Dominators in DAGs for Path-Covering Problems. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 55:1-55:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{sena_et_al:LIPIcs.ESA.2025.55,
author = {Sena, Francisco and Rizzi, Romeo and Tomescu, Alexandru I.},
title = {{Safe Sequences via Dominators in DAGs for Path-Covering Problems}},
booktitle = {33rd Annual European Symposium on Algorithms (ESA 2025)},
pages = {55:1--55:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-395-9},
ISSN = {1868-8969},
year = {2025},
volume = {351},
editor = {Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.55},
URN = {urn:nbn:de:0030-drops-245230},
doi = {10.4230/LIPIcs.ESA.2025.55},
annote = {Keywords: directed acyclic graph, path cover, dominator tree, integer linear programming, least squares, minimum path error}
}
Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)
Loukas Georgiadis, Konstantinos Giannis, and Giuseppe F. Italiano. Faster Dynamic 2-Edge Connectivity in Directed Graphs. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{georgiadis_et_al:LIPIcs.ESA.2025.26,
author = {Georgiadis, Loukas and Giannis, Konstantinos and Italiano, Giuseppe F.},
title = {{Faster Dynamic 2-Edge Connectivity in Directed Graphs}},
booktitle = {33rd Annual European Symposium on Algorithms (ESA 2025)},
pages = {26:1--26:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-395-9},
ISSN = {1868-8969},
year = {2025},
volume = {351},
editor = {Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.26},
URN = {urn:nbn:de:0030-drops-244945},
doi = {10.4230/LIPIcs.ESA.2025.26},
annote = {Keywords: Connectivity, dynamic algorithms, directed graphs}
}
Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)
Md. Hasin Abrar, Paul Medvedev, and Giorgio Vinciguerra. Efficiency of Learned Indexes on Genome Spectra. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 18:1-18:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{abrar_et_al:LIPIcs.ESA.2025.18,
author = {Abrar, Md. Hasin and Medvedev, Paul and Vinciguerra, Giorgio},
title = {{Efficiency of Learned Indexes on Genome Spectra}},
booktitle = {33rd Annual European Symposium on Algorithms (ESA 2025)},
pages = {18:1--18:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-395-9},
ISSN = {1868-8969},
year = {2025},
volume = {351},
editor = {Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.18},
URN = {urn:nbn:de:0030-drops-244865},
doi = {10.4230/LIPIcs.ESA.2025.18},
annote = {Keywords: Genome spectra, piecewise linear approximation, learned index, k-mers}
}
Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)
Jean Cardinal and Yelena Yuditsky. Compact Representation of Semilinear and Terrain-Like Graphs. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 67:1-67:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{cardinal_et_al:LIPIcs.ESA.2025.67,
author = {Cardinal, Jean and Yuditsky, Yelena},
title = {{Compact Representation of Semilinear and Terrain-Like Graphs}},
booktitle = {33rd Annual European Symposium on Algorithms (ESA 2025)},
pages = {67:1--67:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-395-9},
ISSN = {1868-8969},
year = {2025},
volume = {351},
editor = {Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.67},
URN = {urn:nbn:de:0030-drops-245359},
doi = {10.4230/LIPIcs.ESA.2025.67},
annote = {Keywords: Biclique covers, intersection graphs, visibility graphs, Zarankiewicz’s problem}
}
Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)
Surender Baswana, Koustav Bhanja, and Anupam Roy. Faster Algorithm for Second (s,t)-Mincut and Breaking Quadratic Barrier for Dual Edge Sensitivity for (s,t)-Mincut. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 68:1-68:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{baswana_et_al:LIPIcs.ESA.2025.68,
author = {Baswana, Surender and Bhanja, Koustav and Roy, Anupam},
title = {{Faster Algorithm for Second (s,t)-Mincut and Breaking Quadratic Barrier for Dual Edge Sensitivity for (s,t)-Mincut}},
booktitle = {33rd Annual European Symposium on Algorithms (ESA 2025)},
pages = {68:1--68:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-395-9},
ISSN = {1868-8969},
year = {2025},
volume = {351},
editor = {Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.68},
URN = {urn:nbn:de:0030-drops-245369},
doi = {10.4230/LIPIcs.ESA.2025.68},
annote = {Keywords: mincut, second mincut, compact structure, fault tolerant, sensitivity oracle, dual edges, st mincut, global mincut, characterization}
}
Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)
Bernhard Haeupler, Yaowei Long, Thatchaphol Saranurak, and Shengzhe Wang. Length-Constrained Directed Expander Decomposition and Length-Constrained Vertex-Capacitated Flow Shortcuts. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 107:1-107:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{haeupler_et_al:LIPIcs.ESA.2025.107,
author = {Haeupler, Bernhard and Long, Yaowei and Saranurak, Thatchaphol and Wang, Shengzhe},
title = {{Length-Constrained Directed Expander Decomposition and Length-Constrained Vertex-Capacitated Flow Shortcuts}},
booktitle = {33rd Annual European Symposium on Algorithms (ESA 2025)},
pages = {107:1--107:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-395-9},
ISSN = {1868-8969},
year = {2025},
volume = {351},
editor = {Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.107},
URN = {urn:nbn:de:0030-drops-245765},
doi = {10.4230/LIPIcs.ESA.2025.107},
annote = {Keywords: Length-Constrained Expander, Expander Decomposition, Shortcut}
}
Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)
Rasmus Kyng, Simon Meierhans, and Gernot Zöcklein. Bootstrapping Dynamic APSP via Sparsification. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 113:1-113:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{kyng_et_al:LIPIcs.ESA.2025.113,
author = {Kyng, Rasmus and Meierhans, Simon and Z\"{o}cklein, Gernot},
title = {{Bootstrapping Dynamic APSP via Sparsification}},
booktitle = {33rd Annual European Symposium on Algorithms (ESA 2025)},
pages = {113:1--113:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-395-9},
ISSN = {1868-8969},
year = {2025},
volume = {351},
editor = {Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.113},
URN = {urn:nbn:de:0030-drops-245826},
doi = {10.4230/LIPIcs.ESA.2025.113},
annote = {Keywords: Dynamic Graph Algorithms, Spanners, Vertex Sparsification, Bootstrapping}
}
Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)
Monika Henzinger, Evangelos Kosinas, Robin Münk, and Harald Räcke. Efficient Contractions of Dynamic Graphs - With Applications. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 36:1-36:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{henzinger_et_al:LIPIcs.ESA.2025.36,
author = {Henzinger, Monika and Kosinas, Evangelos and M\"{u}nk, Robin and R\"{a}cke, Harald},
title = {{Efficient Contractions of Dynamic Graphs - With Applications}},
booktitle = {33rd Annual European Symposium on Algorithms (ESA 2025)},
pages = {36:1--36:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-395-9},
ISSN = {1868-8969},
year = {2025},
volume = {351},
editor = {Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.36},
URN = {urn:nbn:de:0030-drops-245047},
doi = {10.4230/LIPIcs.ESA.2025.36},
annote = {Keywords: Graph Algorithms, Cut Sparsifiers, Dynamic Algorithms}
}
Published in: LIPIcs, Volume 351, 33rd Annual European Symposium on Algorithms (ESA 2025)
Laxman Dhulipala, Monika Henzinger, George Z. Li, Quanquan C. Liu, A. R. Sricharan, and Leqi Zhu. Near-Optimal Differentially Private Graph Algorithms via the Multidimensional AboveThreshold Mechanism. In 33rd Annual European Symposium on Algorithms (ESA 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 351, pp. 91:1-91:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{dhulipala_et_al:LIPIcs.ESA.2025.91,
author = {Dhulipala, Laxman and Henzinger, Monika and Li, George Z. and Liu, Quanquan C. and Sricharan, A. R. and Zhu, Leqi},
title = {{Near-Optimal Differentially Private Graph Algorithms via the Multidimensional AboveThreshold Mechanism}},
booktitle = {33rd Annual European Symposium on Algorithms (ESA 2025)},
pages = {91:1--91:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-395-9},
ISSN = {1868-8969},
year = {2025},
volume = {351},
editor = {Benoit, Anne and Kaplan, Haim and Wild, Sebastian and Herman, Grzegorz},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2025.91},
URN = {urn:nbn:de:0030-drops-245601},
doi = {10.4230/LIPIcs.ESA.2025.91},
annote = {Keywords: differential privacy, abovethreshold, densest subgraph}
}
Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)
Chase Norman and Jeremy Avigad. Canonical for Automated Theorem Proving in Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 14:1-14:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@InProceedings{norman_et_al:LIPIcs.ITP.2025.14,
author = {Norman, Chase and Avigad, Jeremy},
title = {{Canonical for Automated Theorem Proving in Lean}},
booktitle = {16th International Conference on Interactive Theorem Proving (ITP 2025)},
pages = {14:1--14: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.14},
URN = {urn:nbn:de:0030-drops-246128},
doi = {10.4230/LIPIcs.ITP.2025.14},
annote = {Keywords: Automated Reasoning, Interactive Theorem Proving, Dependent Type Theory, Inhabitation, Unification, Program Synthesis, Formal Methods}
}