Burak Ekici, Tadayoshi Kamegai, Nobuko Yoshida. Subject Reduction and Progress for Synchronous MPST (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-24677,
title = {{Subject Reduction and Progress for Synchronous MPST}},
author = {Ekici, Burak and Kamegai, Tadayoshi and Yoshida, Nobuko},
note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:dde907697cf2446177177fa14a2d21b1c08149f5;origin=https://github.com/Apiros3/smpst-sr-smer;visit=swh:1:snp:3a02010b54199925764021babd0e391fa180a01b;anchor=swh:1:rev:583edde920ef3833382ff6c9130f0d20db90744b}{\texttt{swh:1:dir:dde907697cf2446177177fa14a2d21b1c08149f5}} (visited on 2025-09-22)},
url = {https://github.com/Apiros3/smpst-sr-smer},
doi = {10.4230/artifacts.24677},
}
Asta Halkjær From, Anders Schlichtkrull. Analytic Completeness (Software, Mechanization). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-23798,
title = {{Analytic Completeness}},
author = {From, Asta Halkj{\ae}r and Schlichtkrull, Anders},
note = {Software, version 1.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:1bea24a089edbdbc233081a23b0dc45963bf6c8f;origin=https://github.com/astahfrom/Analytic_Completeness;visit=swh:1:snp:1c9ea048be7f3b4c9f6ed573e2d87ba0b8480717;anchor=swh:1:rev:cd6a06dd8478287763c6e820e51581322faa7f2c}{\texttt{swh:1:dir:1bea24a089edbdbc233081a23b0dc45963bf6c8f}} (visited on 2025-09-22)},
url = {https://github.com/astahfrom/Analytic_Completeness},
doi = {10.4230/artifacts.23798},
}
Yves Bertot, Thomas Portet. math-comp trajectories (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{suppl_material,
title = {{math-comp trajectories}},
author = {Bertot, Yves and Portet, Thomas},
note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:169acc62d26af37f236ba047dc5b75b7cc68fadb;origin=https://github.com/math-comp/trajectories;visit=swh:1:snp:6281f4cd4361a2b27e4d3dbd240f501f358e9adc;anchor=swh:1:rev:31e3a5cb7fbc46dc1ebcc988cee711a0bb01fc53}{\texttt{swh:1:dir:169acc62d26af37f236ba047dc5b75b7cc68fadb}} (visited on 2025-09-22)},
url = {https://github.com/math-comp/trajectories/tree/vertical-cells-paper},
doi = {10.4230/artifacts.24678},
}
Zhuo Zoey Chen, Johannes Åman Pohjola, Christine Rizkallah. cbpv-reasonable-HOL (Software, Mechanised Proof). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-24718,
title = {{cbpv-reasonable-HOL}},
author = {Chen, Zhuo Zoey and \r{A}man Pohjola, Johannes and Rizkallah, Christine},
note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:df18377e9fa5e35255f2687ad66ddbc2f010b934;origin=https://github.com/ZhuoZoeyChen/cbpv-reasonable-HOL;visit=swh:1:snp:9fefd6f03db3694a8bdc7e5ea8ff0f4a1fbde680;anchor=swh:1:rev:4e4f4692c9e6e1e23c566ec4730f81eafde32f3c}{\texttt{swh:1:dir:df18377e9fa5e35255f2687ad66ddbc2f010b934}} (visited on 2025-09-22)},
url = {https://github.com/ZhuoZoeyChen/cbpv-reasonable-HOL/},
doi = {10.4230/artifacts.24718},
}
Stefania Damato, Thorsten Altenkirch, Axel Ljungström. stefaniatadama/formalising-inductive-coinductive-containers (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-24710,
title = {{stefaniatadama/formalising-inductive-coinductive-containers}},
author = {Damato, Stefania and Altenkirch, Thorsten and Ljungstr\"{o}m, Axel},
note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:a75b7ddaa46ca9a9f3ee6f65d22ba3b1c959d6d4;origin=https://github.com/stefaniatadama/formalising-inductive-coinductive-containers;visit=swh:1:snp:eebf2acbd002c4877bc6057e65e8ddef2b0fe79e;anchor=swh:1:rev:4e587677bdc0c7cb793ad8612c1e6e88c16877e7}{\texttt{swh:1:dir:a75b7ddaa46ca9a9f3ee6f65d22ba3b1c959d6d4}} (visited on 2025-09-22)},
url = {https://github.com/stefaniatadama/formalising-inductive-coinductive-containers/blob/main/cubical/Cubical/Papers/Containers.agda},
doi = {10.4230/artifacts.24710},
}
Joshua M. Cohen. Proof Artifact for "A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching" (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{artifact,
title = {{Proof Artifact for "A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching"}},
author = {Cohen, Joshua M.},
note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:31808a21d5034756c3c2d3fc11b22697aaf6eee9;origin=https://doi.org/10.5281/zenodo.15838909;visit=swh:1:snp:eb7de80ce7ad282da1b64dafeea97454bc2f8111;anchor=swh:1:rel:95ec4913f8d066f491fc6864223ddc5539e2eefb;path=/joscoh-why3-semantics-14cabf2/}{\texttt{swh:1:dir:31808a21d5034756c3c2d3fc11b22697aaf6eee9}} (visited on 2025-09-22)},
url = {https://github.com/joscoh/why3-semantics/tree/itp25},
doi = {10.4230/artifacts.24696},
}
@misc{dagpub-supp--paper-23340-urlgithub.com-knothed-CompCert-ct,
title = {{CompCert+PCFL}},
author = {Knothe, David},
note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:521e7528bd5a40751111337e04cc57d469e0dd6b;origin=https://github.com/knothed/CompCert-ct;visit=swh:1:snp:9160a96825d7e1ecdfe276dc8033660174b771c6;anchor=swh:1:rev:2d1369a4888cff6fd5fd29f28a059e9cf72b1a08}{\texttt{swh:1:dir:521e7528bd5a40751111337e04cc57d469e0dd6b}} (visited on 2025-09-22)},
url = {https://github.com/knothed/CompCert-ct},
}
Jonas Bayer, Marco David, Théo André, Mathis Bouverot-Dupuis, Eva Brenner, Loïc Chevalier, Anna Danilkin, Charlotte Dorneich, Kevin Lee, Xavier Pigé, Timothé Ringeard, Quentin Vermande, Paul Wang, Annie Yao, Zhengkun Ye. Universal Pairs for Diophantine Equations (Software, Formal Proof Development). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-24709,
title = {{Universal Pairs for Diophantine Equations }},
author = {Bayer, Jonas and David, Marco and Andr\'{e}, Th\'{e}o and Bouverot-Dupuis, Mathis and Brenner, Eva and Chevalier, Lo\"{i}c and Danilkin, Anna and Dorneich, Charlotte and Lee, Kevin and Pig\'{e}, Xavier and Ringeard, Timoth\'{e} and Vermande, Quentin and Wang, Paul and Yao, Annie and Ye, Zhengkun},
note = {Software (visited on 2025-09-22)},
url = {https://www.isa-afp.org/entries/Diophantine_Universal_Pairs.html},
doi = {10.4230/artifacts.24709},
}
David Castro Perez, Marco Paviotti, Michael Vollmer. dcastrop/coq-hylomorphisms (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-23907,
title = {{dcastrop/coq-hylomorphisms}},
author = {Castro Perez, David and Paviotti, Marco and Vollmer, Michael},
note = {Software, EP/Y00339X/1, EP/T014512/1, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:72a5871702972010658c8b75970475a540abf44d;origin=https://github.com/dcastrop/coq-hylomorphisms;visit=swh:1:snp:3033a9703c61e14e58b51c7f66c784b9955e737f;anchor=swh:1:rev:305c425fdd165254bbf1bee47ed9d44d6b93fa3c}{\texttt{swh:1:dir:72a5871702972010658c8b75970475a540abf44d}} (visited on 2025-09-22)},
url = {https://github.com/dcastrop/coq-hylomorphisms},
doi = {10.4230/artifacts.23907},
}
Johannes Tantow, Lukas Gerlach, Stephan Mennicke, Markus Krötzsch. knowsys/CertifyingDatalog (Software, Lean Formalization). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-23826,
title = {{knowsys/CertifyingDatalog}},
author = {Tantow, Johannes and Gerlach, Lukas and Mennicke, Stephan and Kr\"{o}tzsch, Markus},
note = {Software, version 0.2.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:57aca8aba4c9f62a87ba52360ad701b8e9cf7b45;origin=https://github.com/knowsys/CertifyingDatalog;visit=swh:1:snp:617e84a1a49818c83a6a7c32cda6267fc6f09596;anchor=swh:1:rev:7adf4abd7826dd529491551f192c5815d430313a}{\texttt{swh:1:dir:57aca8aba4c9f62a87ba52360ad701b8e9cf7b45}} (visited on 2025-09-22)},
url = {https://github.com/knowsys/CertifyingDatalog/tree/v0.2.0},
doi = {10.4230/artifacts.23826},
}
Chase Norman. Canonical (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-24703,
title = {{Canonical}},
author = {Norman, Chase},
note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:06a599989bad108dc52bfdff704d356badfa63d4;origin=https://github.com/chasenorman/Canonical;visit=swh:1:snp:b14b45164fd97819d6c472ac9195bf01ab92047c;anchor=swh:1:rev:d5c7fd0d8d0f1a2e4d8eed817d534725ea8e1156}{\texttt{swh:1:dir:06a599989bad108dc52bfdff704d356badfa63d4}} (visited on 2025-09-22)},
url = {https://github.com/chasenorman/Canonical},
doi = {10.4230/artifacts.24703},
}
Chase Norman. CanonicalLean (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-24708,
title = {{CanonicalLean}},
author = {Norman, Chase},
note = {Software, version v4.22.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:98f9920f9b96cabe1c6188b23fd3823d0ad9fb0f;origin=https://github.com/chasenorman/Canonicallean;visit=swh:1:snp:944ef1c9397eb4eb6dc2e6e7d500f38c3033a5ea;anchor=swh:1:rev:65797c0994b252ecca26934afe92766147fedbd3}{\texttt{swh:1:dir:98f9920f9b96cabe1c6188b23fd3823d0ad9fb0f}} (visited on 2025-09-22)},
url = {https://github.com/chasenorman/CanonicalLean},
doi = {10.4230/artifacts.24708},
}
Adrienne Lancelot, Beniamino Accattoli, Maxime Vemclefs. adrilancelot/Abella-lambda-Barendregt-theory (Software, Abella formalization code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{AbellaSources,
title = {{adrilancelot/Abella-lambda-Barendregt-theory}},
author = {Lancelot, Adrienne and Accattoli, Beniamino and Vemclefs, Maxime},
note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:b20ffd2d8d946adac1eb2fffa72112d23a2deeed;origin=https://github.com/adrilancelot/Abella-lambda-Barendregt-theory;visit=swh:1:snp:51adf802a55fe82840e4e8d940b31babccdb58a2;anchor=swh:1:rev:07ea3f03983145ce1b7e070e3afbe9ff730d2531}{\texttt{swh:1:dir:b20ffd2d8d946adac1eb2fffa72112d23a2deeed}} (visited on 2025-09-22)},
url = {https://github.com/adrilancelot/Abella-lambda-Barendregt-theory},
doi = {10.4230/artifacts.23906},
}
Hippolyte Hilgers, Radu-Daniel Vatavu. Project XXR: Novel Extended Reality Models and Software Framework for Interactive Environments with Extreme Conditions, http://www.eed.usv.ro/mintviz/projects/XXR/ (Dataset, Spreadsheet with raw data, statistical and inferential analyses, and charts). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-24337,
title = {{Project XXR: Novel Extended Reality Models and Software Framework for Interactive Environments with Extreme Conditions, http://www.eed.usv.ro/mintviz/projects/XXR/}},
author = {Hilgers, Hippolyte and Vatavu, Radu-Daniel},
note = {Dataset, version 1.0. (visited on 2025-09-21)},
url = {http://www.kaggle.com/datasets/jeanvanderdonckt/dataset-spacechi2025-paper},
doi = {10.4230/artifacts.24337},
}
Sven Jörissen, David L. Hilbert, Michael Bleier, Dorit Borrmann, Helge A. Lauterbach, Andreas Nüchter. Underwater VR for Astronaut Training (Audiovisual, video demonstrating the approach). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)
@misc{dagstuhl-artifact-24343,
title = {{Underwater VR for Astronaut Training}},
author = {J\"{o}rissen, Sven and Hilbert, David L. and Bleier, Michael and Borrmann, Dorit and Lauterbach, Helge A. and N\"{u}chter, Andreas},
note = {Audiovisual (visited on 2025-09-21)},
url = {https://youtu.be/rKG1XqJKrDw},
doi = {10.4230/artifacts.24343},
}
Feedback for Dagstuhl Publishing