9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)

<!DOCTYPE html> <html lang="en"> <head> <meta charset="utf-8" /> <meta http-equiv="X-UA-Compatible" content="IE=edge" /> <meta name="google" content="notranslate"> <meta http-equiv="Content-Language" content="en"> <meta name="viewport" content="width=device-width, initial-scale=1" /> <meta name="csrf-token" content="iF3j5hXd6Qsj4qBbXp9S7Ibul72S8iuAU3rm0vf0" /> <link rel="canonical" href="https://drops.dagstuhl.de/entities/volume/LIPIcs-volume-211" /> <title>9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)</title> <link rel="icon" href="https://drops.dagstuhl.de/favicon.ico" /> <link rel="stylesheet" href="https://drops.dagstuhl.de/css/app.css?drops-core-2024-10-22" /> </head> <body> <nav class="navbar main fixed-top navbar-expand-lg navbar-light bg-light"> <div class="container-fluid"> <a class="navbar-brand" href="https://www.dagstuhl.de"> <img class="lzi-logo" src="https://drops.dagstuhl.de/images/LZI-Logo.jpg" width="84" height=62" alt="Schloss Dagstuhl - LZI - Logo" /> </a> <button class="navbar-toggler" type="button" data-bs-toggle="collapse" data-bs-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation"> <span class="navbar-toggler-icon"></span> </button> <div class="collapse navbar-collapse" id="navbarSupportedContent"> <ul class="navbar-nav me-auto mb-2 mb-lg-0"> <li class="nav-item" style="white-space: nowrap"> <a class="nav-link" href="https://drops.dagstuhl.de"> <i class="bi bi-house large-icon"></i> DROPS </a> </li> <li class="nav-item dropdown"> <a class="nav-link dropdown-toggle" href="#" id="navbarDropdownSeries" role="button" data-bs-toggle="dropdown" aria-expanded="false"> <i class="bi bi-journals large-icon"></i> Series </a> <ul class="dropdown-menu" aria-labelledby="navbarDropdown"> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/series/LIPIcs"> LIPIcs – Leibniz International Proceedings in Informatics </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/series/OASIcs"> OASIcs – Open Access Series in Informatics </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/series/DFU"> Dagstuhl Follow-Ups </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/series/DagAnnRep"> Schloss Dagstuhl Jahresbericht </a> </li> <li class="dropdown-divider"></li> <li> <a class="dropdown-item" href="/#discontinued-series">Discontinued Series</a> </li> </ul> </li> <li class="nav-item dropdown"> <a class="nav-link dropdown-toggle" href="#" id="navbarDropdownJournals" role="button" data-bs-toggle="dropdown" aria-expanded="false"> <i class="bi bi-journal large-icon"></i> Journals </a> <ul class="dropdown-menu" aria-labelledby="navbarDropdown"> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/journal/DARTS"> DARTS – Dagstuhl Artifacts Series </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/journal/DagRep"> Dagstuhl Reports </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/journal/DagMan"> Dagstuhl Manifestos </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/journal/LITES"> LITES – Leibniz Transactions on Embedded Systems </a> </li> <li><a class="dropdown-item" href="https://drops.dagstuhl.de/entities/journal/TGDK"> TGDK – Transactions on Graph Data and Knowledge </a> </li> </ul> </li> <li class="nav-item dropdown"> <a class="nav-link dropdown-toggle" href="#" id="navbarDropdownConferences" role="button" data-bs-toggle="dropdown" aria-expanded="false"> <i class="bi bi-people large-icon"></i> Conferences </a> <ul class="dropdown-menu conference-dropdown" aria-labelledby="navbarDropdown"> <div class="row"> <div class="col-sm-4 nav-conference-col"> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/AFT"> AFT </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/AIB"> AIB </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/AofA"> AofA </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/APPROX"> APPROX </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ATMOS"> ATMOS </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/CALCO"> CALCO </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/CCC"> CCC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/CONCUR"> CONCUR </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/COSIT"> COSIT </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/CP"> CP </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/CPM"> CPM </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/CSL"> CSL </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/DISC"> DISC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/DITAM"> DITAM </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/DNA"> DNA </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ECOOP"> ECOOP </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ECRTS"> ECRTS </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ESA"> ESA </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/FAB"> FAB </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/FMBC"> FMBC </a> </li> </div> <div class="col-sm-4 nav-conference-col"> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/FORC"> FORC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/FSCD"> FSCD </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/FSTTCS"> FSTTCS </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/FUN"> FUN </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/GD"> GD </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/GIScience"> GIScience </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ICALP"> ICALP </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ICDT"> ICDT </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ICPEC"> ICPEC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/IPEC"> IPEC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/iPMVM"> iPMVM </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ISAAC"> ISAAC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ITC"> ITC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ITCS"> ITCS </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/ITP"> ITP </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/LDK"> LDK </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/MFCS"> MFCS </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/Microservices"> Microservices </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/NG-RES"> NG-RES </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/OPODIS"> OPODIS </a> </li> </div> <div class="col-sm-4 nav-conference-col"> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/PARMA"> PARMA </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/RANDOM"> RANDOM </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SAND"> SAND </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SAT"> SAT </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SEA"> SEA </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SLATE"> SLATE </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SNAPL"> SNAPL </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SoCG"> SoCG </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/STACS"> STACS </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/SWAT"> SWAT </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/TIME"> TIME </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/Tokenomics"> Tokenomics </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/TQC"> TQC </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/TYPES"> TYPES </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/WABI"> WABI </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/conference/WCET"> WCET </a> </li> </div> </div> </ul> </li> <li class="nav-item"> <a class="nav-link" href="https://drops.dagstuhl.de/docs/about" id="navbarAbout"> <i class="bi bi-info-circle large-icon"></i><span class="nav-text-about-drops"> About DROPS</span> </a> </li> </ul> <form class="navbar-search d-flex" action="https://drops.dagstuhl.de/search" method="post"> <input type="hidden" name="_token" value="iF3j5hXd6Qsj4qBbXp9S7Ibul72S8iuAU3rm0vf0" autocomplete="off"> <div class="input-group"> <input class="form-control" type="search" placeholder="Search" aria-label="Search" name="term" autocomplete="off" maxlength="600"> <button class="btn btn-outline-success" type="submit"> <i class="bi bi-search" style="color: #000"></i> </button> </div> </form> <ul class="navbar-nav nav-metadata"> <li class="nav-item dropdown"> <a class="nav-link dropdown-toggle" id="navbarDropdownMetadata" role="button" data-bs-toggle="dropdown" aria-expanded="false"> <i class="bi bi-database-down large-icon"></i><span class="nav-text-metadata">Metadata Export</span> </a> <ul class="dropdown-menu dropdown-metadata" aria-labelledby="navbarDropdownMetadata"> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/metadata">Metadata Export</a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/oai?verb=Identify" target="_blank">OAI Interface</a> </li> </ul> </li> </ul> </div> </div> </nav> <div id="app" data-release="drops-core-2024-10-22" class="container "> <div id="_top-of-page"></div> <div class="fixed-search-button"><i class="bi bi-search"></i></div> <div class="volume-portal"> <br> <div class="entity-type volume"> <div> <span class="entity-type-name"> <i class="bi bi-book-half"></i> Volume </span> <span class="sharing-section"> <span class="sharing-buttons"> <span class="dropdown"> <a class="btn sharing-btn metadata dropdown-toggle" href="#" role="button" data-bs-toggle="dropdown" aria-expanded="false"><i class="bi bi-download"></i></a> <ul class="dropdown-menu dropdown-menu-end"> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/volume/LIPIcs-volume-211/metadata/xml"> Export XML </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/volume/LIPIcs-volume-211/metadata/acm-xml"> Export ACM-XML </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/volume/LIPIcs-volume-211/metadata/doaj-xml"> Export DOAJ-XML </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/volume/LIPIcs-volume-211/metadata/schema-org"> Export Schema.org </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/volume/LIPIcs-volume-211/metadata/bibtex"> Export BibTeX </a> </li> <li> <a class="dropdown-item" href="https://drops.dagstuhl.de/entities/volume/LIPIcs-volume-211/metadata/html"> Export HTML </a> </li> </ul> </span> </span> </span> </div> </div> <hr> <div> <h4>LIPIcs, Volume 211</h4> <h1>9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)</h1> </div> <section class="volume-issue-header mb-4"> <hr/> <section class="is-part-of"> <ul> <li> <span>Part of:</span> <span style="white-space: nowrap"> <i class="bi bi-journals"></i> Series: </span> <a href="https://drops.dagstuhl.de/entities/series/LIPIcs">Leibniz International Proceedings in Informatics (LIPIcs)</a> <br> <span style="visibility: hidden">Part of:</span> <span style="white-space: nowrap"> <i class="bi bi-people"></i> Conference: </span> <a href="https://drops.dagstuhl.de/entities/conference/CALCO">Conference on Algebra and Coalgebra in Computer Science (CALCO)</a> </li> </ul> </section> <hr/> <div class="mt-5 row"> <div class="col-lg-3 mb-3"> <section class="thumbnail"> <img src="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/thumbnails/LIPIcs.CALCO.2021/LIPIcs.CALCO.2021.png" alt="Thumbnail PDF" /> </section> </div> <div class="col-lg-6"> <section class="mb-5"> <h4>Event</h4> <a href="https://www.coalg.org/calco-mfps2021/calco/"> CALCO 2021, August 31 to September 3, 2021, Salzburg, Austria </a> </section> <section class="editors mb-5"> <h4>Editors</h4> <div class="author person-details"> <div> <span class="name"><b>Fabio Gadducci</b></span> <a href="https://orcid.org/0000-0003-0690-3051"><img class="orcid-logo" src="https://drops.dagstuhl.de/images/orcid.png" alt="ORCID-Logo"></a> <a href="mailto:fabio.gadducci@unipi.it"><i class="bi bi-envelope"></i></a> <a href="https://drops.dagstuhl.de/search/documents?author=Gadducci, Fabio"><small><i class="bi bi-search"></i></small></a> </div> <ul> <li class="affiliation">University of Pisa, Italy</li> </ul> </div> <div class="author person-details"> <div> <span class="name"><b>Alexandra Silva</b></span> <a href="https://orcid.org/0000-0001-5014-9784"><img class="orcid-logo" src="https://drops.dagstuhl.de/images/orcid.png" alt="ORCID-Logo"></a> <a href="mailto:alexandra.silva@gmail.com"><i class="bi bi-envelope"></i></a> <a href="https://drops.dagstuhl.de/search/documents?author=Silva, Alexandra"><small><i class="bi bi-search"></i></small></a> </div> <ul> <li class="affiliation">Cornell University, USA</li> <li class="affiliation">University College London, UK</li> </ul> </div> </section> </div> <div class="col-lg-3"> <section class="mb-5"> <h4>Publication Details</h4> <ul> <li>published at: 2021-11-08</li> <li>Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik</li> <li>ISBN: 978-3-95977-212-9</li> <li>DBLP: <a href="https://dblp.org/db/conf/calco/calco2021"> db/conf/calco/calco2021 </a> </li> </ul> </section> <br> <section> <h4>Access Numbers</h4> <ul> <li> <a href="#" class="btn-statistics" data-entity="volume/LIPIcs-volume-211" data-title="9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)"> <i class="bi bi-graph-up"></i> Detailed Access Statistics available here </a> </li> <li> Total Document Accesses (updated on a weekly basis): <div class="stats-total"> <div class="stats total-downloads"> <div class="circle"> <div class="number" data-number="0">0</div> </div> <div class="label">PDF Downloads</div> </div> <div class="stats total-metadata-views"> <div class="circle"> <div class="number" data-number="0">0</div> </div> <div class="label">Metadata Views</div> </div> </div>  </li> </ul> </section> </div> </div> <div id="end-of-header"></div> </section> <div class="row mt-2"> <div class="col-sm-9 mt-2"> <h2>Documents <span class="btn badge color-dark _filter-info"></span></h2> <div class="documents"> <div class="no-results alert alert-danger -hidden"> No documents found matching your filter selection. </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">Complete Volume</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021">DOI: 10.4230/LIPIcs.CALCO.2021</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021/LIPIcs.CALCO.2021.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15775" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15775" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021" data-bs-toggle="tooltip" data-title="LIPIcs, Volume 211, CALCO 2021, Complete Volume" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Gadducci, Fabio"></span> <span data-key="dagstuhl.contributor.author" data-value="Silva, Alexandra"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Models of computation"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Modal and temporal logics"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Algebraic semantics"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Categorical semantics"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Quantum computation theory"></span> <span data-key="dagstuhl.subject.classification" data-value="Software and its engineering → Context specific languages"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021"> LIPIcs, Volume 211, CALCO 2021, Complete Volume </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Fabio Gadducci and Alexandra Silva </p> <div class="row"> <div class="collapse" id="abstract-15775"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15775">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> LIPIcs, Volume 211, CALCO 2021, Complete Volume </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15775"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15775">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 1-384, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15775-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@Proceedings{gadducci_et_al:LIPIcs.CALCO.2021, title = {{LIPIcs, Volume 211, CALCO 2021, Complete Volume}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {1--384}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021}, URN = {urn:nbn:de:0030-drops-153544}, doi = {10.4230/LIPIcs.CALCO.2021}, annote = {Keywords: LIPIcs, Volume 211, CALCO 2021, Complete Volume} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15775-input">@Proceedings{gadducci_et_al:LIPIcs.CALCO.2021, title = {{LIPIcs, Volume 211, CALCO 2021, Complete Volume}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {1--384}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021}, URN = {urn:nbn:de:0030-drops-153544}, doi = {10.4230/LIPIcs.CALCO.2021}, annote = {Keywords: LIPIcs, Volume 211, CALCO 2021, Complete Volume} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.0"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">Front Matter</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.0">DOI: 10.4230/LIPIcs.CALCO.2021.0</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.0/LIPIcs.CALCO.2021.0.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.0" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15776" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15776" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.0" data-bs-toggle="tooltip" data-title="Front Matter, Table of Contents, Preface, Conference Organization" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Gadducci, Fabio"></span> <span data-key="dagstuhl.contributor.author" data-value="Silva, Alexandra"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Models of computation"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Modal and temporal logics"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Algebraic semantics"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Categorical semantics"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Quantum computation theory"></span> <span data-key="dagstuhl.subject.classification" data-value="Software and its engineering → Context specific languages"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.0"> Front Matter, Table of Contents, Preface, Conference Organization </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Fabio Gadducci and Alexandra Silva </p> <div class="row"> <div class="collapse" id="abstract-15776"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15776">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> Front Matter, Table of Contents, Preface, Conference Organization </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15776"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15776">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15776-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{gadducci_et_al:LIPIcs.CALCO.2021.0, author = {Gadducci, Fabio and Silva, Alexandra}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {0:i--0:x}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.0}, URN = {urn:nbn:de:0030-drops-153559}, doi = {10.4230/LIPIcs.CALCO.2021.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15776-input">@InProceedings{gadducci_et_al:LIPIcs.CALCO.2021.0, author = {Gadducci, Fabio and Silva, Alexandra}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {0:i--0:x}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.0}, URN = {urn:nbn:de:0030-drops-153559}, doi = {10.4230/LIPIcs.CALCO.2021.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.1"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">Invited Talk</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.1">DOI: 10.4230/LIPIcs.CALCO.2021.1</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.1/LIPIcs.CALCO.2021.1.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.1" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15777" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15777" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.1" data-bs-toggle="tooltip" data-title="Distributive Laws for Lawvere Theories (Invited Talk)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Cheng, Eugenia"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Semantics and reasoning"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.1"> Distributive Laws for Lawvere Theories (Invited Talk) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Eugenia Cheng </p> <div class="row"> <div class="collapse" id="abstract-15777"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15777">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> Distributive laws give a way of combining two algebraic structures expressed as monads; in this work we propose a theory of distributive laws for combining algebraic structures expressed as Lawvere theories. We propose four approaches, involving profunctors, monoidal profunctors, an extension of the free finite-product category 2-monad from Cat to Prof, and factorisation systems respectively. We exhibit comparison functors between CAT and each of these new frameworks to show that the distributive laws between the Lawvere theories correspond in a suitable way to distributive laws between their associated finitary monads. The different but equivalent formulations then provide, between them, a framework conducive to generalisation, but also an explicit description of the composite theories arising from distributive laws. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15777"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15777">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Eugenia Cheng. Distributive Laws for Lawvere Theories (Invited Talk). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15777-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{cheng:LIPIcs.CALCO.2021.1, author = {Cheng, Eugenia}, title = {{Distributive Laws for Lawvere Theories}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {1:1--1:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.1}, URN = {urn:nbn:de:0030-drops-153560}, doi = {10.4230/LIPIcs.CALCO.2021.1}, annote = {Keywords: Distributive laws, Monads, Lawvere theories} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15777-input">@InProceedings{cheng:LIPIcs.CALCO.2021.1, author = {Cheng, Eugenia}, title = {{Distributive Laws for Lawvere Theories}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {1:1--1:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.1}, URN = {urn:nbn:de:0030-drops-153560}, doi = {10.4230/LIPIcs.CALCO.2021.1}, annote = {Keywords: Distributive laws, Monads, Lawvere theories} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.2"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">Invited Talk</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.2">DOI: 10.4230/LIPIcs.CALCO.2021.2</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.2/LIPIcs.CALCO.2021.2.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.2" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15778" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15778" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.2" data-bs-toggle="tooltip" data-title="Towards Engineering Smart Cyber-Physical Systems with Graph Transformation Systems (Invited Talk)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Giese, Holger"></span> <span data-key="dagstuhl.subject.classification" data-value="Software and its engineering → Software notations and tools"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.2"> Towards Engineering Smart Cyber-Physical Systems with Graph Transformation Systems (Invited Talk) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Holger Giese </p> <div class="row"> <div class="collapse" id="abstract-15778"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15778">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> A dramatic transformation of our technical world towards smart cyber-physical systems can be currently observed. This transformation results in a networked technical world where besides the embedded systems with their interaction with the physical world the interconnection of these nodes in the cyber world becomes a key element. Furthermore, there is a strong trend towards smart systems where artificial intelligence techniques and in particular machine learning is employed to make software behave accordingly. This raises the question whether our capabilities to model these future embedded systems are ready to tackle the resulting challenges. In this presentation, we will first discuss how extensions of graph transformation systems can be employed to design and analyse the envisioned future cyber-physical systems with an emphasis on the synergies networking can offer and then characterise which challenges for the design, production, and operation of these systems and how they can be tacked with graph transformation systems. We will therefore discuss to what extent our current capabilities in particular concerning engineering with graph transformation systems match these challenges and where substantial improvements for the graph transformation systems have been crucial and will be crucial in the future. Models are used in classical engineering to plan systems upfront to maximise envisioned properties resp. minimise cost. For smart cyber-physical systems this decoupling of development-time and run-time considerations vanishes, and self-adaptation and runtime models have been advocated as concepts to shift some considerations to run-time. We will review the underlying causes for this shift to run-time, discuss some our work with graph transformation systems in this direction, and outline related open challenges and implications for future work for graph transformation systems to engineer smart cyber-physical systems. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15778"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15778">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Holger Giese. Towards Engineering Smart Cyber-Physical Systems with Graph Transformation Systems (Invited Talk). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15778-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{giese:LIPIcs.CALCO.2021.2, author = {Giese, Holger}, title = {{Towards Engineering Smart Cyber-Physical Systems with Graph Transformation Systems}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.2}, URN = {urn:nbn:de:0030-drops-153573}, doi = {10.4230/LIPIcs.CALCO.2021.2}, annote = {Keywords: Cyber-physical systems, Graph transformation} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15778-input">@InProceedings{giese:LIPIcs.CALCO.2021.2, author = {Giese, Holger}, title = {{Towards Engineering Smart Cyber-Physical Systems with Graph Transformation Systems}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {2:1--2:1}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.2}, URN = {urn:nbn:de:0030-drops-153573}, doi = {10.4230/LIPIcs.CALCO.2021.2}, annote = {Keywords: Cyber-physical systems, Graph transformation} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.3"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">Invited Talk</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.3">DOI: 10.4230/LIPIcs.CALCO.2021.3</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.3/LIPIcs.CALCO.2021.3.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.3" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15779" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15779" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.3" data-bs-toggle="tooltip" data-title="Dialectica Comonads (Invited Talk)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="de Paiva, Valeria"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Logic"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.3"> Dialectica Comonads (Invited Talk) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Valeria de Paiva </p> <div class="row"> <div class="collapse" id="abstract-15779"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15779">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> Dialectica categories are interesting categorical models of Linear Logic which preserve the differences between linear connectives that the logic is supposed to make, unlike some of the most traditional models like coherence spaces. They arise from the categorical modelling of Gödel’s Dialectica interpretation and seem to be having a revival: connections between Dialectica constructions and containers, lenses and polynomials have been described recently in the literature. In this note I will recap the basic Dialectica constructions and then go on to describe the less well-known interplay of comonads, coalgebras and comonoids that characterizes the composite functor standing for the "of course!" operator in dialectica categories. This composition of comonads evokes some work on stateful games by Laird and others, also discussed in the setting of Reddy’s system LLMS (Linear Logic Model of State). </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15779"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15779">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Valeria de Paiva. Dialectica Comonads (Invited Talk). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 3:1-3:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15779-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{depaiva:LIPIcs.CALCO.2021.3, author = {de Paiva, Valeria}, title = {{Dialectica Comonads}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {3:1--3:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.3}, URN = {urn:nbn:de:0030-drops-153581}, doi = {10.4230/LIPIcs.CALCO.2021.3}, annote = {Keywords: Dialectica categories, Linear logic, Comonads} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15779-input">@InProceedings{depaiva:LIPIcs.CALCO.2021.3, author = {de Paiva, Valeria}, title = {{Dialectica Comonads}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {3:1--3:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.3}, URN = {urn:nbn:de:0030-drops-153581}, doi = {10.4230/LIPIcs.CALCO.2021.3}, annote = {Keywords: Dialectica categories, Linear logic, Comonads} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.4"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">Invited Talk</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.4">DOI: 10.4230/LIPIcs.CALCO.2021.4</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.4/LIPIcs.CALCO.2021.4.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.4" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15780" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15780" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.4" data-bs-toggle="tooltip" data-title="The Challenges of Weak Persistency (Invited Talk)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Vafeiadis, Viktor"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Logic and verification"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.4"> The Challenges of Weak Persistency (Invited Talk) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Viktor Vafeiadis </p> <div class="row"> <div class="collapse" id="abstract-15780"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15780">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> Non-volatile memory (NVM) is a new hardware technology that provides durable storage at performance similar to that of plain volatile RAM. As such, there is a lot of interest in exploiting this technology to improve the performance of existing disk-bound applications and to find new applications for it. Nevertheless, developing correct programs that interact with non-volatile memory is by no means easy, since mainstream architectures provide rather weak persistency semantics and rather low-level and expensive mechanisms in order to avoid weak behaviors. This creates many opportunities for researchers in programming language semantics, logic, and verification to develop techniques to assist programmers writing NVM programs. This short paper and the associated talk outline the challenges caused by NVM and the research opportunities for PL researchers. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15780"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15780">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Viktor Vafeiadis. The Challenges of Weak Persistency (Invited Talk). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15780-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{vafeiadis:LIPIcs.CALCO.2021.4, author = {Vafeiadis, Viktor}, title = {{The Challenges of Weak Persistency}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {4:1--4:3}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.4}, URN = {urn:nbn:de:0030-drops-153593}, doi = {10.4230/LIPIcs.CALCO.2021.4}, annote = {Keywords: Weak Persistency, Non-Volatile Memory} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15780-input">@InProceedings{vafeiadis:LIPIcs.CALCO.2021.4, author = {Vafeiadis, Viktor}, title = {{The Challenges of Weak Persistency}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {4:1--4:3}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.4}, URN = {urn:nbn:de:0030-drops-153593}, doi = {10.4230/LIPIcs.CALCO.2021.4}, annote = {Keywords: Weak Persistency, Non-Volatile Memory} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.5"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">(Co)algebraic pearls</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.5">DOI: 10.4230/LIPIcs.CALCO.2021.5</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.5/LIPIcs.CALCO.2021.5.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.5" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15781" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15781" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.5" data-bs-toggle="tooltip" data-title="Initial Algebras Without Iteration ((Co)algebraic pearls)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Adámek, Jiří"></span> <span data-key="dagstuhl.contributor.author" data-value="Milius, Stefan"></span> <span data-key="dagstuhl.contributor.author" data-value="Moss, Lawrence S."></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Models of computation"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Logic and verification"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.5"> Initial Algebras Without Iteration ((Co)algebraic pearls) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Jiří Adámek, Stefan Milius, and Lawrence S. Moss </p> <div class="row"> <div class="collapse" id="abstract-15781"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15781">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> The Initial Algebra Theorem by Trnková et al. states, under mild assumptions, that an endofunctor has an initial algebra provided it has a pre-fixed point. The proof crucially depends on transfinitely iterating the functor and in fact shows that, equivalently, the (transfinite) initial-algebra chain stops. We give a constructive proof of the Initial Algebra Theorem that avoids transfinite iteration of the functor. For a given pre-fixed point A of the functor, it uses Pataraia’s theorem to obtain the least fixed point of a monotone function on the partial order formed by all subobjects of A. Thanks to properties of recursive coalgebras, this least fixed point yields an initial algebra. We obtain new results on fixed points and initial algebras in categories enriched over directed-complete partial orders, again without iteration. Using transfinite iteration we equivalently obtain convergence of the initial-algebra chain as an equivalent condition, overall yielding a streamlined version of the original proof. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15781"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15781">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Initial Algebras Without Iteration ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15781-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{adamek_et_al:LIPIcs.CALCO.2021.5, author = {Ad\'{a}mek, Ji\v{r}{\'\i} and Milius, Stefan and Moss, Lawrence S.}, title = {{Initial Algebras Without Iteration}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {5:1--5:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.5}, URN = {urn:nbn:de:0030-drops-153606}, doi = {10.4230/LIPIcs.CALCO.2021.5}, annote = {Keywords: Initial algebra, Pataraia’s theorem, recursive coalgebra, initial-algebra chain} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15781-input">@InProceedings{adamek_et_al:LIPIcs.CALCO.2021.5, author = {Ad\'{a}mek, Ji\v{r}{\'\i} and Milius, Stefan and Moss, Lawrence S.}, title = {{Initial Algebras Without Iteration}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {5:1--5:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.5}, URN = {urn:nbn:de:0030-drops-153606}, doi = {10.4230/LIPIcs.CALCO.2021.5}, annote = {Keywords: Initial algebra, Pataraia’s theorem, recursive coalgebra, initial-algebra chain} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.6"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">(Co)algebraic pearls</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.6">DOI: 10.4230/LIPIcs.CALCO.2021.6</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.6/LIPIcs.CALCO.2021.6.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.6" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15782" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15782" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.6" data-bs-toggle="tooltip" data-title="Which Categories Are Varieties? ((Co)algebraic pearls)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Adámek, Jiří"></span> <span data-key="dagstuhl.contributor.author" data-value="Rosický, Jiří"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Algebraic language theory"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.6"> Which Categories Are Varieties? ((Co)algebraic pearls) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Jiří Adámek and Jiří Rosický </p> <div class="row"> <div class="collapse" id="abstract-15782"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15782">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> Categories equivalent to single-sorted varieties of finitary algebras were characterized in the famous dissertation of Lawvere. We present a new proof of a slightly sharpened version: those are precisely the categories with kernel pairs and reflexive coequalizers having an abstractly finite, effective strong generator. A completely analogous result is proved for varieties of many-sorted algebras provided that there are only finitely many sorts. In case of infinitely many sorts a slightly weaker result is presented: instead of being abstractly finite, the generator is required to consist of finitely presentable objects. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15782"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15782">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Jiří Adámek and Jiří Rosický. Which Categories Are Varieties? ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 6:1-6:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15782-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{adamek_et_al:LIPIcs.CALCO.2021.6, author = {Ad\'{a}mek, Ji\v{r}{\'\i} and Rosick\'{y}, Ji\v{r}{\'\i}}, title = {{Which Categories Are Varieties?}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {6:1--6:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.6}, URN = {urn:nbn:de:0030-drops-153610}, doi = {10.4230/LIPIcs.CALCO.2021.6}, annote = {Keywords: variety, many-sorted algebra, abstractly finite object, effective object, strong generator} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15782-input">@InProceedings{adamek_et_al:LIPIcs.CALCO.2021.6, author = {Ad\'{a}mek, Ji\v{r}{\'\i} and Rosick\'{y}, Ji\v{r}{\'\i}}, title = {{Which Categories Are Varieties?}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {6:1--6:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.6}, URN = {urn:nbn:de:0030-drops-153610}, doi = {10.4230/LIPIcs.CALCO.2021.6}, annote = {Keywords: variety, many-sorted algebra, abstractly finite object, effective object, strong generator} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.7"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.7">DOI: 10.4230/LIPIcs.CALCO.2021.7</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.7/LIPIcs.CALCO.2021.7.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.7" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15783" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15783" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.7" data-bs-toggle="tooltip" data-title="Tensor of Quantitative Equational Theories" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Bacci, Giorgio"></span> <span data-key="dagstuhl.contributor.author" data-value="Mardare, Radu"></span> <span data-key="dagstuhl.contributor.author" data-value="Panangaden, Prakash"></span> <span data-key="dagstuhl.contributor.author" data-value="Plotkin, Gordon"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Equational logic and rewriting"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.7"> Tensor of Quantitative Equational Theories </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin </p> <div class="row"> <div class="collapse" id="abstract-15783"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15783">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> We develop a theory for the commutative combination of quantitative effects, their tensor, given as a combination of quantitative equational theories that imposes mutual commutation of the operations from each theory. As such, it extends the sum of two theories, which is just their unrestrained combination. Tensors of theories arise in several contexts; in particular, in the semantics of programming languages, the monad transformer for global state is given by a tensor. We show that under certain assumptions on the quantitative theories the free monad that arises from the tensor of two theories is the categorical tensor of the free monads on the theories. As an application, we provide the first algebraic axiomatizations of labelled Markov processes and Markov decision processes. Apart from the intrinsic interest in the axiomatizations, it is pleasing they are obtained compositionally by means of the sum and tensor of simpler quantitative equational theories. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15783"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15783">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Giorgio Bacci, Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Tensor of Quantitative Equational Theories. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 7:1-7:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15783-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{bacci_et_al:LIPIcs.CALCO.2021.7, author = {Bacci, Giorgio and Mardare, Radu and Panangaden, Prakash and Plotkin, Gordon}, title = {{Tensor of Quantitative Equational Theories}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {7:1--7:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.7}, URN = {urn:nbn:de:0030-drops-153628}, doi = {10.4230/LIPIcs.CALCO.2021.7}, annote = {Keywords: Quantitative equational theories, Tensor, Monads, Quantitative Effects} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15783-input">@InProceedings{bacci_et_al:LIPIcs.CALCO.2021.7, author = {Bacci, Giorgio and Mardare, Radu and Panangaden, Prakash and Plotkin, Gordon}, title = {{Tensor of Quantitative Equational Theories}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {7:1--7:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.7}, URN = {urn:nbn:de:0030-drops-153628}, doi = {10.4230/LIPIcs.CALCO.2021.7}, annote = {Keywords: Quantitative equational theories, Tensor, Monads, Quantitative Effects} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.8"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.8">DOI: 10.4230/LIPIcs.CALCO.2021.8</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.8/LIPIcs.CALCO.2021.8.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.8" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15784" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15784" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.8" data-bs-toggle="tooltip" data-title="Pushdown Automata and Context-Free Grammars in Bisimulation Semantics" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Baeten, Jos C. M."></span> <span data-key="dagstuhl.contributor.author" data-value="Carissimo, Cesare"></span> <span data-key="dagstuhl.contributor.author" data-value="Luttik, Bas"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Interactive computation"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Turing machines"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Grammars and context-free languages"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Process calculi"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.8"> Pushdown Automata and Context-Free Grammars in Bisimulation Semantics </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Jos C. M. Baeten, Cesare Carissimo, and Bas Luttik </p> <div class="row"> <div class="collapse" id="abstract-15784"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15784">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> The Turing machine models an old-fashioned computer, that does not interact with the user or with other computers, and only does batch processing. Therefore, we came up with a Reactive Turing Machine that does not have these shortcomings. In the Reactive Turing Machine, transitions have labels to give a notion of interactivity. In the resulting process graph, we use bisimilarity instead of language equivalence. Subsequently, we considered other classical theorems and notions from automata theory and formal languages theory. In this paper, we consider the classical theorem of the correspondence between pushdown automata and context-free grammars. By changing the process operator of sequential composition to a sequencing operator with intermediate acceptance, we get a better correspondence in our setting. We find that the missing ingredient to recover the full correspondence is the addition of a notion of state awareness. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15784"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15784">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Jos C. M. Baeten, Cesare Carissimo, and Bas Luttik. Pushdown Automata and Context-Free Grammars in Bisimulation Semantics. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 8:1-8:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15784-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{baeten_et_al:LIPIcs.CALCO.2021.8, author = {Baeten, Jos C. M. and Carissimo, Cesare and Luttik, Bas}, title = {{Pushdown Automata and Context-Free Grammars in Bisimulation Semantics}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {8:1--8:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.8}, URN = {urn:nbn:de:0030-drops-153632}, doi = {10.4230/LIPIcs.CALCO.2021.8}, annote = {Keywords: pushdown automaton, context-free grammar, bisimilarity, intermediate acceptance, state awareness} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15784-input">@InProceedings{baeten_et_al:LIPIcs.CALCO.2021.8, author = {Baeten, Jos C. M. and Carissimo, Cesare and Luttik, Bas}, title = {{Pushdown Automata and Context-Free Grammars in Bisimulation Semantics}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {8:1--8:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.8}, URN = {urn:nbn:de:0030-drops-153632}, doi = {10.4230/LIPIcs.CALCO.2021.8}, annote = {Keywords: pushdown automaton, context-free grammar, bisimilarity, intermediate acceptance, state awareness} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.9"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">(Co)algebraic pearls</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.9">DOI: 10.4230/LIPIcs.CALCO.2021.9</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.9/LIPIcs.CALCO.2021.9.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.9" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15785" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15785" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.9" data-bs-toggle="tooltip" data-title="From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra ((Co)algebraic pearls)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Bonchi, Filippo"></span> <span data-key="dagstuhl.contributor.author" data-value="Di Giorgio, Alessandro"></span> <span data-key="dagstuhl.contributor.author" data-value="Zanasi, Fabio"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Categorical semantics"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.9"> From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra ((Co)algebraic pearls) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Filippo Bonchi, Alessandro Di Giorgio, and Fabio Zanasi </p> <div class="row"> <div class="collapse" id="abstract-15785"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15785">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> Farkas' lemma is a celebrated result on the solutions of systems of linear inequalities, which finds application pervasively in mathematics and computer science. In this work we show how to formulate and prove Farkas' lemma in diagrammatic polyhedral algebra, a sound and complete graphical calculus for polyhedra. Furthermore, we show how linear programs can be modeled within the calculus and how some famous duality results can be proved. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15785"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15785">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Filippo Bonchi, Alessandro Di Giorgio, and Fabio Zanasi. From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 9:1-9:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15785-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.9, author = {Bonchi, Filippo and Di Giorgio, Alessandro and Zanasi, Fabio}, title = {{From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {9:1--9:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.9}, URN = {urn:nbn:de:0030-drops-153643}, doi = {10.4230/LIPIcs.CALCO.2021.9}, annote = {Keywords: String diagrams, Farkas Lemma, Duality, Linear Programming} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15785-input">@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.9, author = {Bonchi, Filippo and Di Giorgio, Alessandro and Zanasi, Fabio}, title = {{From Farkas' Lemma to Linear Programming: an Exercise in Diagrammatic Algebra}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {9:1--9:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.9}, URN = {urn:nbn:de:0030-drops-153643}, doi = {10.4230/LIPIcs.CALCO.2021.9}, annote = {Keywords: String diagrams, Farkas Lemma, Duality, Linear Programming} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.10"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.10">DOI: 10.4230/LIPIcs.CALCO.2021.10</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.10/LIPIcs.CALCO.2021.10.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.10" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15786" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15786" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.10" data-bs-toggle="tooltip" data-title="On Doctrines and Cartesian Bicategories" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Bonchi, Filippo"></span> <span data-key="dagstuhl.contributor.author" data-value="Santamaria, Alessio"></span> <span data-key="dagstuhl.contributor.author" data-value="Seeber, Jens"></span> <span data-key="dagstuhl.contributor.author" data-value="Sobociński, Paweł"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Logic"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Categorical semantics"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.10"> On Doctrines and Cartesian Bicategories </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Paweł Sobociński </p> <div class="row"> <div class="collapse" id="abstract-15786"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15786">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> We study the relationship between cartesian bicategories and a specialisation of Lawvere’s hyperdoctrines, namely elementary existential doctrines. Both provide different ways of abstracting the structural properties of logical systems: the former in algebraic terms based on a string diagrammatic calculus, the latter in universal terms using the fundamental notion of adjoint functor. We prove that these two approaches are related by an adjunction, which can be strengthened to an equivalence by imposing further constraints on doctrines. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15786"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15786">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Filippo Bonchi, Alessio Santamaria, Jens Seeber, and Paweł Sobociński. On Doctrines and Cartesian Bicategories. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 10:1-10:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15786-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.10, author = {Bonchi, Filippo and Santamaria, Alessio and Seeber, Jens and Soboci\'{n}ski, Pawe{\l}}, title = {{On Doctrines and Cartesian Bicategories}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {10:1--10:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.10}, URN = {urn:nbn:de:0030-drops-153656}, doi = {10.4230/LIPIcs.CALCO.2021.10}, annote = {Keywords: Cartesian bicategories, elementary existential doctrines, string diagram} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15786-input">@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.10, author = {Bonchi, Filippo and Santamaria, Alessio and Seeber, Jens and Soboci\'{n}ski, Pawe{\l}}, title = {{On Doctrines and Cartesian Bicategories}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {10:1--10:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.10}, URN = {urn:nbn:de:0030-drops-153656}, doi = {10.4230/LIPIcs.CALCO.2021.10}, annote = {Keywords: Cartesian bicategories, elementary existential doctrines, string diagram} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.11"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">(Co)algebraic pearls</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.11">DOI: 10.4230/LIPIcs.CALCO.2021.11</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.11/LIPIcs.CALCO.2021.11.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.11" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15787" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15787" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.11" data-bs-toggle="tooltip" data-title="Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases ((Co)algebraic pearls)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Bonchi, Filippo"></span> <span data-key="dagstuhl.contributor.author" data-value="Sokolova, Ana"></span> <span data-key="dagstuhl.contributor.author" data-value="Vignudelli, Valeria"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Logic and verification"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Axiomatic semantics"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Categorical semantics"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.11"> Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases ((Co)algebraic pearls) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli </p> <div class="row"> <div class="collapse" id="abstract-15787"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15787">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> We prove that every finitely generated convex set of finitely supported probability distributions has a unique base. We apply this result to provide an alternative proof of a recent result: the algebraic theory of convex semilattices presents the monad of convex sets of probability distributions. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15787"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15787">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15787-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.11, author = {Bonchi, Filippo and Sokolova, Ana and Vignudelli, Valeria}, title = {{Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {11:1--11:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.11}, URN = {urn:nbn:de:0030-drops-153666}, doi = {10.4230/LIPIcs.CALCO.2021.11}, annote = {Keywords: Convex sets of distributions monad, Convex semilattices, Unique base} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15787-input">@InProceedings{bonchi_et_al:LIPIcs.CALCO.2021.11, author = {Bonchi, Filippo and Sokolova, Ana and Vignudelli, Valeria}, title = {{Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {11:1--11:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.11}, URN = {urn:nbn:de:0030-drops-153666}, doi = {10.4230/LIPIcs.CALCO.2021.11}, annote = {Keywords: Convex sets of distributions monad, Convex semilattices, Unique base} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.12"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.12">DOI: 10.4230/LIPIcs.CALCO.2021.12</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.12/LIPIcs.CALCO.2021.12.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.12" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15788" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15788" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.12" data-bs-toggle="tooltip" data-title="Closure Hyperdoctrines" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Castelnovo, Davide"></span> <span data-key="dagstuhl.contributor.author" data-value="Miculan, Marino"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Modal and temporal logics"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.12"> Closure Hyperdoctrines </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Davide Castelnovo and Marino Miculan </p> <div class="row"> <div class="collapse" id="abstract-15788"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15788">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> (Pre)closure spaces are a generalization of topological spaces covering also the notion of neighbourhood in discrete structures, widely used to model and reason about spatial aspects of distributed systems. In this paper we present an abstract theoretical framework for the systematic investigation of the logical aspects of closure spaces. To this end, we introduce the notion of closure (hyper)doctrines, i.e. doctrines endowed with inflationary operators (and subject to suitable conditions). The generality and effectiveness of this concept is witnessed by many examples arising naturally from topological spaces, fuzzy sets, algebraic structures, coalgebras, and covering at once also known cases such as Kripke frames and probabilistic frames (i.e., Markov chains). By leveraging general categorical constructions, we provide axiomatisations and sound and complete semantics for various fragments of logics for closure operators. Hence, closure hyperdoctrines are useful both for refining and improving the theory of existing spatial logics, and for the definition of new spatial logics for new applications. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15788"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15788">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Davide Castelnovo and Marino Miculan. Closure Hyperdoctrines. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 12:1-12:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15788-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{castelnovo_et_al:LIPIcs.CALCO.2021.12, author = {Castelnovo, Davide and Miculan, Marino}, title = {{Closure Hyperdoctrines}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {12:1--12:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.12}, URN = {urn:nbn:de:0030-drops-153678}, doi = {10.4230/LIPIcs.CALCO.2021.12}, annote = {Keywords: categorical logic, topological semantics, closure operators, spatial logic} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15788-input">@InProceedings{castelnovo_et_al:LIPIcs.CALCO.2021.12, author = {Castelnovo, Davide and Miculan, Marino}, title = {{Closure Hyperdoctrines}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {12:1--12:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.12}, URN = {urn:nbn:de:0030-drops-153678}, doi = {10.4230/LIPIcs.CALCO.2021.12}, annote = {Keywords: categorical logic, topological semantics, closure operators, spatial logic} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.13"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">(Co)algebraic pearls</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.13">DOI: 10.4230/LIPIcs.CALCO.2021.13</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.13/LIPIcs.CALCO.2021.13.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.13" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15789" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15789" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.13" data-bs-toggle="tooltip" data-title="How to Write a Coequation ((Co)algebraic pearls)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Dahlqvist, Fredrik"></span> <span data-key="dagstuhl.contributor.author" data-value="Schmid, Todd"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Modal and temporal logics"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Formal languages and automata theory"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Program specifications"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.13"> How to Write a Coequation ((Co)algebraic pearls) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Fredrik Dahlqvist and Todd Schmid </p> <div class="row"> <div class="collapse" id="abstract-15789"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15789">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> There is a large amount of literature on the topic of covarieties, coequations and coequational specifications, dating back to the early seventies. Nevertheless, coequations have not (yet) emerged as an everyday practical specification formalism for computer scientists. In this review paper, we argue that this is partly due to the multitude of syntaxes for writing down coequations, which seems to have led to some confusion about what coequations are and what they are for. By surveying the literature, we identify four types of syntaxes: coequations-as-corelations, coequations-as-predicates, coequations-as-equations, and coequations-as-modal-formulas. We present each of these in a tutorial fashion, relate them to each other, and discuss their respective uses. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15789"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15789">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Fredrik Dahlqvist and Todd Schmid. How to Write a Coequation ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 13:1-13:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15789-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{dahlqvist_et_al:LIPIcs.CALCO.2021.13, author = {Dahlqvist, Fredrik and Schmid, Todd}, title = {{How to Write a Coequation}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {13:1--13:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.13}, URN = {urn:nbn:de:0030-drops-153686}, doi = {10.4230/LIPIcs.CALCO.2021.13}, annote = {Keywords: Coalgebra, coequation, covariety} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15789-input">@InProceedings{dahlqvist_et_al:LIPIcs.CALCO.2021.13, author = {Dahlqvist, Fredrik and Schmid, Todd}, title = {{How to Write a Coequation}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {13:1--13:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.13}, URN = {urn:nbn:de:0030-drops-153686}, doi = {10.4230/LIPIcs.CALCO.2021.13}, annote = {Keywords: Coalgebra, coequation, covariety} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.14"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.14">DOI: 10.4230/LIPIcs.CALCO.2021.14</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.14/LIPIcs.CALCO.2021.14.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.14" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15790" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15790" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.14" data-bs-toggle="tooltip" data-title="Monads on Categories of Relational Structures" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Ford, Chase"></span> <span data-key="dagstuhl.contributor.author" data-value="Milius, Stefan"></span> <span data-key="dagstuhl.contributor.author" data-value="Schröder, Lutz"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Models of computation"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Logic and verification"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.14"> Monads on Categories of Relational Structures </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Chase Ford, Stefan Milius, and Lutz Schröder </p> <div class="row"> <div class="collapse" id="abstract-15790"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15790">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> We introduce a framework for universal algebra in categories of relational structures given by finitary relational signatures and finitary or infinitary Horn theories, with the arity λ of a Horn theory understood as a strict upper bound on the number of premisses in its axioms; key examples include partial orders (λ = ω) or metric spaces (λ = ω₁). We establish a bijective correspondence between λ-accessible enriched monads on the given category of relational structures and a notion of λ-ary algebraic theories (i.e. with operations of arity < λ), with the syntax of algebraic theories induced by the relational signature (e.g. inequations or equations-up-to-ε). We provide a generic sound and complete derivation system for such relational algebraic theories, thus in particular recovering (extensions of) recent systems of this type for monads on partial orders and metric spaces by instantiation. In particular, we present an ω₁-ary algebraic theory of metric completion. The theory-to-monad direction of our correspondence remains true for the case of κ-ary algebraic theories and κ-accessible monads for κ < λ, e.g. for finitary theories over metric spaces. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15790"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15790">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Chase Ford, Stefan Milius, and Lutz Schröder. Monads on Categories of Relational Structures. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15790-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{ford_et_al:LIPIcs.CALCO.2021.14, author = {Ford, Chase and Milius, Stefan and Schr\"{o}der, Lutz}, title = {{Monads on Categories of Relational Structures}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {14:1--14:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.14}, URN = {urn:nbn:de:0030-drops-153697}, doi = {10.4230/LIPIcs.CALCO.2021.14}, annote = {Keywords: monads, relational structures, Horn theories, relational logic} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15790-input">@InProceedings{ford_et_al:LIPIcs.CALCO.2021.14, author = {Ford, Chase and Milius, Stefan and Schr\"{o}der, Lutz}, title = {{Monads on Categories of Relational Structures}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {14:1--14:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.14}, URN = {urn:nbn:de:0030-drops-153697}, doi = {10.4230/LIPIcs.CALCO.2021.14}, annote = {Keywords: monads, relational structures, Horn theories, relational logic} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.15"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.15">DOI: 10.4230/LIPIcs.CALCO.2021.15</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.15/LIPIcs.CALCO.2021.15.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.15" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15791" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15791" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.15" data-bs-toggle="tooltip" data-title="Stream Processors and Comodels" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Garner, Richard"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Categorical semantics"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Automata over infinite objects"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.15"> Stream Processors and Comodels </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Richard Garner </p> <div class="row"> <div class="collapse" id="abstract-15791"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15791">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> In 2009, Ghani, Hancock and Pattinson gave a coalgebraic characterisation of stream processors A^ℕ → B^ℕ drawing on ideas of Brouwerian constructivism. Their stream processors have an intensional character; in this paper, we give a corresponding coalgebraic characterisation of extensional stream processors, i.e., the set of continuous functions A^ℕ → B^ℕ. Our account sites both our result and that of op. cit. within the apparatus of comodels for algebraic effects originating with Power-Shkaravska. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15791"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15791">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Richard Garner. Stream Processors and Comodels. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15791-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{garner:LIPIcs.CALCO.2021.15, author = {Garner, Richard}, title = {{Stream Processors and Comodels}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {15:1--15:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.15}, URN = {urn:nbn:de:0030-drops-153700}, doi = {10.4230/LIPIcs.CALCO.2021.15}, annote = {Keywords: Comodels, residual comodels, bimodels, streams, stream processors} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15791-input">@InProceedings{garner:LIPIcs.CALCO.2021.15, author = {Garner, Richard}, title = {{Stream Processors and Comodels}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {15:1--15:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.15}, URN = {urn:nbn:de:0030-drops-153700}, doi = {10.4230/LIPIcs.CALCO.2021.15}, annote = {Keywords: Comodels, residual comodels, bimodels, streams, stream processors} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.16"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.16">DOI: 10.4230/LIPIcs.CALCO.2021.16</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.16/LIPIcs.CALCO.2021.16.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.16" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15792" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15792" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.16" data-bs-toggle="tooltip" data-title="A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Grabmayer, Clemens"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Process calculi"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.16"> A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Clemens Grabmayer </p> <div class="row"> <div class="collapse" id="abstract-15792"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15792">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> By adapting Salomaa’s complete proof system for equality of regular expressions under the language semantics, Milner (1984) formulated a sound proof system for bisimilarity of regular expressions under the process interpretation he introduced. He asked whether this system is complete. Proof-theoretic arguments attempting to show completeness of this equational system are complicated by the presence of a non-algebraic rule for solving fixed-point equations by using star iteration. We characterize the derivational power that the fixed-point rule adds to the purely equational part Mil- of Milner’s system Mil: it corresponds to the power of coinductive proofs over Mil- that have the form of finite process graphs with the loop existence and elimination property LEE. We define a variant system cMil by replacing the fixed-point rule in Mil with a rule that permits LEE-shaped circular derivations in Mil- from previously derived equations as a premise. With this rule alone we also define the variant system CLC for combining LEE-shaped coinductive proofs over Mil-. We show that both cMil and CLC have proof interpretations in Mil, and vice versa. As this correspondence links, in both directions, derivability in Mil with derivation trees of process graphs, it widens the space for graph-based approaches to finding a completeness proof of Milner’s system. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15792"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15792">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Clemens Grabmayer. A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 16:1-16:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15792-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{grabmayer:LIPIcs.CALCO.2021.16, author = {Grabmayer, Clemens}, title = {{A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {16:1--16:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.16}, URN = {urn:nbn:de:0030-drops-153712}, doi = {10.4230/LIPIcs.CALCO.2021.16}, annote = {Keywords: regular expressions, process theory, bisimilarity, coinduction, proof theory} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15792-input">@InProceedings{grabmayer:LIPIcs.CALCO.2021.16, author = {Grabmayer, Clemens}, title = {{A Coinductive Version of Milner’s Proof System for Regular Expressions Modulo Bisimilarity}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {16:1--16:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.16}, URN = {urn:nbn:de:0030-drops-153712}, doi = {10.4230/LIPIcs.CALCO.2021.16}, annote = {Keywords: regular expressions, process theory, bisimilarity, coinduction, proof theory} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.17"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.17">DOI: 10.4230/LIPIcs.CALCO.2021.17</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.17/LIPIcs.CALCO.2021.17.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.17" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15793" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15793" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.17" data-bs-toggle="tooltip" data-title="Functorial Semantics as a Unifying Perspective on Logic Programming" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Gu, Tao"></span> <span data-key="dagstuhl.contributor.author" data-value="Zanasi, Fabio"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Categorical semantics"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.17"> Functorial Semantics as a Unifying Perspective on Logic Programming </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Tao Gu and Fabio Zanasi </p> <div class="row"> <div class="collapse" id="abstract-15793"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15793">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> Logic programming and its variations are widely used for formal reasoning in various areas of Computer Science, most notably Artificial Intelligence. In this paper we develop a systematic and unifying perspective for (ground) classical, probabilistic, weighted logic programs, based on categorical algebra. Our departure point is a formal distinction between the syntax and the semantics of programs, now regarded as separate categories. Then, we are able to characterise the various variants of logic program as different models for the same syntax category, i.e. structure-preserving functors in the spirit of Lawvere’s functorial semantics. As a first consequence of our approach, we showcase a series of semantic constructs for logic programming pictorially as certain string diagrams in the syntax category. Secondly, we describe the correspondence between probabilistic logic programs and Bayesian networks in terms of the associated models. Our analysis reveals that the correspondence can be phrased in purely syntactical terms, without resorting to the probabilistic domain of interpretation. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15793"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15793">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Tao Gu and Fabio Zanasi. Functorial Semantics as a Unifying Perspective on Logic Programming. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 17:1-17:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15793-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{gu_et_al:LIPIcs.CALCO.2021.17, author = {Gu, Tao and Zanasi, Fabio}, title = {{Functorial Semantics as a Unifying Perspective on Logic Programming}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {17:1--17:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.17}, URN = {urn:nbn:de:0030-drops-153723}, doi = {10.4230/LIPIcs.CALCO.2021.17}, annote = {Keywords: string diagrams, functorial semantics, logic programming} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15793-input">@InProceedings{gu_et_al:LIPIcs.CALCO.2021.17, author = {Gu, Tao and Zanasi, Fabio}, title = {{Functorial Semantics as a Unifying Perspective on Logic Programming}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {17:1--17:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.17}, URN = {urn:nbn:de:0030-drops-153723}, doi = {10.4230/LIPIcs.CALCO.2021.17}, annote = {Keywords: string diagrams, functorial semantics, logic programming} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.18"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">Early Ideas</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.18">DOI: 10.4230/LIPIcs.CALCO.2021.18</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.18/LIPIcs.CALCO.2021.18.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.18" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15794" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15794" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.18" data-bs-toggle="tooltip" data-title="The Central Valuations Monad (Early Ideas)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Jia, Xiaodong"></span> <span data-key="dagstuhl.contributor.author" data-value="Mislove, Michael"></span> <span data-key="dagstuhl.contributor.author" data-value="Zamdzhiev, Vladimir"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Denotational semantics"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.18"> The Central Valuations Monad (Early Ideas) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Xiaodong Jia, Michael Mislove, and Vladimir Zamdzhiev </p> <div class="row"> <div class="collapse" id="abstract-15794"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15794">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> We give a commutative valuations monad Z on the category DCPO of dcpo’s and Scott-continuous functions. Compared to the commutative valuations monads given in [Xiaodong Jia et al., 2021], our new monad Z is larger and it contains all push-forward images of valuations on the unit interval [0, 1] along lower semi-continuous maps. We believe that this new monad will be useful in giving domain-theoretic denotational semantics for statistical programming languages with continuous probabilistic choice. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15794"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15794">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Xiaodong Jia, Michael Mislove, and Vladimir Zamdzhiev. The Central Valuations Monad (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 18:1-18:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15794-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{jia_et_al:LIPIcs.CALCO.2021.18, author = {Jia, Xiaodong and Mislove, Michael and Zamdzhiev, Vladimir}, title = {{The Central Valuations Monad}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {18:1--18:5}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.18}, URN = {urn:nbn:de:0030-drops-153733}, doi = {10.4230/LIPIcs.CALCO.2021.18}, annote = {Keywords: Valuations, Commutative Monad, DCPO, Probabilistic Choice, Recursion} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15794-input">@InProceedings{jia_et_al:LIPIcs.CALCO.2021.18, author = {Jia, Xiaodong and Mislove, Michael and Zamdzhiev, Vladimir}, title = {{The Central Valuations Monad}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {18:1--18:5}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.18}, URN = {urn:nbn:de:0030-drops-153733}, doi = {10.4230/LIPIcs.CALCO.2021.18}, annote = {Keywords: Valuations, Commutative Monad, DCPO, Probabilistic Choice, Recursion} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.19"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.19">DOI: 10.4230/LIPIcs.CALCO.2021.19</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.19/LIPIcs.CALCO.2021.19.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.19" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15795" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15795" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.19" data-bs-toggle="tooltip" data-title="Coderelictions for Free Exponential Modalities" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Lemay, Jean-Simon Pacaud"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Categorical semantics"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Linear logic"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.19"> Coderelictions for Free Exponential Modalities </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Jean-Simon Pacaud Lemay </p> <div class="row"> <div class="collapse" id="abstract-15795"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15795">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> In a categorical model of the multiplicative and exponential fragments of intuitionistic linear logic (MELL), the exponential modality is interpreted as a comonad ! such that each cofree !-coalgebra !A comes equipped with a natural cocommutative comonoid structure. An important case is when ! is a free exponential modality so that !A is the cofree cocommutative comonoid over A. A categorical model of MELL with a free exponential modality is called a Lafont category. A categorical model of differential linear logic is called a differential category, where the differential structure can equivalently be described by a deriving transformation !A⊗A →{𝖽_A} !A or a codereliction A →{η_A} !A. Blute, Lucyshyn-Wright, and O'Neill showed that every Lafont category with finite biproducts is a differential category. However, from a differential linear logic perspective, Blute, Lucyshyn-Wright, and O'Neill’s approach is not the usual one since the result was stated in the dual setting and the proof is in terms of the deriving transformation 𝖽. In differential linear logic, it is often the codereliction η that is preferred and that plays a more prominent role. In this paper, we provide an alternative proof that every Lafont category (with finite biproducts) is a differential category, where we construct the codereliction η using the couniversal property of the cofree cocommtuative comonoid !A and show that η is unique. To achieve this, we introduce the notion of an infinitesimal augmentation k⊕A →{𝖧_A} !(k ⊕ A), which in particular is a !-coalgebra and a comonoid morphism, and show that infinitesimal augmentations are in bijective correspondence to coderelictions (and deriving transformations). As such, infinitesimal augmentations provide a new equivalent axiomatization for differential categories in terms of more commonly known concepts. For a free exponential modality, its infinitesimal augmentation is easy to construct and allows one to clearly see the differential structure of a Lafont category, regardless of the construction of !A. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15795"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15795">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Jean-Simon Pacaud Lemay. Coderelictions for Free Exponential Modalities. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 19:1-19:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15795-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{lemay:LIPIcs.CALCO.2021.19, author = {Lemay, Jean-Simon Pacaud}, title = {{Coderelictions for Free Exponential Modalities}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {19:1--19:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.19}, URN = {urn:nbn:de:0030-drops-153742}, doi = {10.4230/LIPIcs.CALCO.2021.19}, annote = {Keywords: Differential Categories, Coderelictions, Differential Linear Logic, Free Exponential Modalities, Lafont Categories, Infinitesimal Augmentations} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15795-input">@InProceedings{lemay:LIPIcs.CALCO.2021.19, author = {Lemay, Jean-Simon Pacaud}, title = {{Coderelictions for Free Exponential Modalities}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {19:1--19:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.19}, URN = {urn:nbn:de:0030-drops-153742}, doi = {10.4230/LIPIcs.CALCO.2021.19}, annote = {Keywords: Differential Categories, Coderelictions, Differential Linear Logic, Free Exponential Modalities, Lafont Categories, Infinitesimal Augmentations} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.20"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.20">DOI: 10.4230/LIPIcs.CALCO.2021.20</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.20/LIPIcs.CALCO.2021.20.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.20" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15796" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15796" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.20" data-bs-toggle="tooltip" data-title="The Open Algebraic Path Problem" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Master, Jade"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Categorical semantics"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Operational semantics"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.20"> The Open Algebraic Path Problem </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Jade Master </p> <div class="row"> <div class="collapse" id="abstract-15796"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15796">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> The algebraic path problem provides a general setting for shortest path algorithms in optimization and computer science. We explain the universal property of solutions to the algebraic path problem by constructing a left adjoint functor whose values are given by these solutions. This paper extends the algebraic path problem to networks equipped with input and output boundaries. We show that the algebraic path problem is functorial as a mapping from a double category whose horizontal composition is gluing of open networks. We introduce functional open matrices, for which the functoriality of the algebraic path problem has a more practical expression. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15796"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15796">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Jade Master. The Open Algebraic Path Problem. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15796-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{master:LIPIcs.CALCO.2021.20, author = {Master, Jade}, title = {{The Open Algebraic Path Problem}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {20:1--20:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.20}, URN = {urn:nbn:de:0030-drops-153754}, doi = {10.4230/LIPIcs.CALCO.2021.20}, annote = {Keywords: The Algebraic Path Problem, Open Systems, Shortest Paths, Categorical Semantics, Compositionality} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15796-input">@InProceedings{master:LIPIcs.CALCO.2021.20, author = {Master, Jade}, title = {{The Open Algebraic Path Problem}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {20:1--20:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.20}, URN = {urn:nbn:de:0030-drops-153754}, doi = {10.4230/LIPIcs.CALCO.2021.20}, annote = {Keywords: The Algebraic Path Problem, Open Systems, Shortest Paths, Categorical Semantics, Compositionality} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.21"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">Early Ideas</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.21">DOI: 10.4230/LIPIcs.CALCO.2021.21</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.21/LIPIcs.CALCO.2021.21.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.21" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15797" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15797" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.21" data-bs-toggle="tooltip" data-title="Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Muroya, Koko"></span> <span data-key="dagstuhl.contributor.author" data-value="Sanada, Takahiro"></span> <span data-key="dagstuhl.contributor.author" data-value="Urabe, Natsuki"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Verification by model checking"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.21"> Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Koko Muroya, Takahiro Sanada, and Natsuki Urabe </p> <div class="row"> <div class="collapse" id="abstract-15797"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15797">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> We describe our ongoing work on generalizing some quantitatively constrained notions of weak simulation up-to that are recently introduced for deterministic systems modeling program execution. We present and discuss a new notion dubbed preorder-constrained simulation that allows comparison between words using a preorder, instead of equality. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15797"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15797">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Koko Muroya, Takahiro Sanada, and Natsuki Urabe. Preorder-Constrained Simulation for Nondeterministic Automata (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 21:1-21:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15797-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{muroya_et_al:LIPIcs.CALCO.2021.21, author = {Muroya, Koko and Sanada, Takahiro and Urabe, Natsuki}, title = {{Preorder-Constrained Simulation for Nondeterministic Automata}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {21:1--21:5}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.21}, URN = {urn:nbn:de:0030-drops-153762}, doi = {10.4230/LIPIcs.CALCO.2021.21}, annote = {Keywords: simulation, weak simulation, up-to technique, language inclusion, preorder} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15797-input">@InProceedings{muroya_et_al:LIPIcs.CALCO.2021.21, author = {Muroya, Koko and Sanada, Takahiro and Urabe, Natsuki}, title = {{Preorder-Constrained Simulation for Nondeterministic Automata}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {21:1--21:5}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.21}, URN = {urn:nbn:de:0030-drops-153762}, doi = {10.4230/LIPIcs.CALCO.2021.21}, annote = {Keywords: simulation, weak simulation, up-to technique, language inclusion, preorder} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.22"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">Early Ideas</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.22">DOI: 10.4230/LIPIcs.CALCO.2021.22</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.22/LIPIcs.CALCO.2021.22.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.22" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15798" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15798" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.22" data-bs-toggle="tooltip" data-title="Quantitative Polynomial Functors (Early Ideas)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Nakov, Georgi"></span> <span data-key="dagstuhl.contributor.author" data-value="Nordvall Forsberg, Fredrik"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Type theory"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Linear logic"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.22"> Quantitative Polynomial Functors (Early Ideas) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Georgi Nakov and Fredrik Nordvall Forsberg </p> <div class="row"> <div class="collapse" id="abstract-15798"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15798">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> We investigate containers and polynomial functors in Quantitative Type Theory, and give initial algebra semantics of inductive data types in the presence of linearity. We show that reasoning by induction is supported, and equivalent to initiality, also in the linear setting. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15798"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15798">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Georgi Nakov and Fredrik Nordvall Forsberg. Quantitative Polynomial Functors (Early Ideas). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 22:1-22:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15798-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{nakov_et_al:LIPIcs.CALCO.2021.22, author = {Nakov, Georgi and Nordvall Forsberg, Fredrik}, title = {{Quantitative Polynomial Functors}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {22:1--22:5}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.22}, URN = {urn:nbn:de:0030-drops-153774}, doi = {10.4230/LIPIcs.CALCO.2021.22}, annote = {Keywords: quantitative type theory, polynomial functors, inductive data types} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15798-input">@InProceedings{nakov_et_al:LIPIcs.CALCO.2021.22, author = {Nakov, Georgi and Nordvall Forsberg, Fredrik}, title = {{Quantitative Polynomial Functors}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {22:1--22:5}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.22}, URN = {urn:nbn:de:0030-drops-153774}, doi = {10.4230/LIPIcs.CALCO.2021.22}, annote = {Keywords: quantitative type theory, polynomial functors, inductive data types} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.23"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">(Co)algebraic pearls</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.23">DOI: 10.4230/LIPIcs.CALCO.2021.23</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.23/LIPIcs.CALCO.2021.23.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.23" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15799" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15799" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.23" data-bs-toggle="tooltip" data-title="Nawrotzki’s Algorithm for the Countable Splitting Lemma, Constructively ((Co)algebraic pearls)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Sokolova, Ana"></span> <span data-key="dagstuhl.contributor.author" data-value="Woracek, Harald"></span> <span data-key="dagstuhl.subject.classification" data-value="Mathematics of computing → Mathematical analysis"></span> <span data-key="dagstuhl.subject.classification" data-value="Mathematics of computing → Probability and statistics"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Design and analysis of algorithms"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Semantics and reasoning"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.23"> Nawrotzki’s Algorithm for the Countable Splitting Lemma, Constructively ((Co)algebraic pearls) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Ana Sokolova and Harald Woracek </p> <div class="row"> <div class="collapse" id="abstract-15799"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15799">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> We reprove the countable splitting lemma by adapting Nawrotzki’s algorithm which produces a sequence that converges to a solution. Our algorithm combines Nawrotzki’s approach with taking finite cuts. It is constructive in the sense that each term of the iteratively built approximating sequence as well as the error between the approximants and the solution is computable with finitely many algebraic operations. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15799"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15799">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Ana Sokolova and Harald Woracek. Nawrotzki’s Algorithm for the Countable Splitting Lemma, Constructively ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15799-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{sokolova_et_al:LIPIcs.CALCO.2021.23, author = {Sokolova, Ana and Woracek, Harald}, title = {{Nawrotzki’s Algorithm for the Countable Splitting Lemma, Constructively}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {23:1--23:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.23}, URN = {urn:nbn:de:0030-drops-153781}, doi = {10.4230/LIPIcs.CALCO.2021.23}, annote = {Keywords: countable splitting lemma, distributions with given marginals, couplings} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15799-input">@InProceedings{sokolova_et_al:LIPIcs.CALCO.2021.23, author = {Sokolova, Ana and Woracek, Harald}, title = {{Nawrotzki’s Algorithm for the Countable Splitting Lemma, Constructively}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {23:1--23:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.23}, URN = {urn:nbn:de:0030-drops-153781}, doi = {10.4230/LIPIcs.CALCO.2021.23}, annote = {Keywords: countable splitting lemma, distributions with given marginals, couplings} }</textarea> </div> </div> </div> </div> <div class="entity-list-item document card m-3" data-show="1" data-permanent-id="document/10.4230/LIPIcs.CALCO.2021.24"> <div class="entity-type"><i class="bi bi-file-earmark"></i> Document</div> <div class="category">(Co)algebraic pearls</div> <div class="doi"><a href="https://doi.org/10.4230/LIPIcs.CALCO.2021.24">DOI: 10.4230/LIPIcs.CALCO.2021.24</a></div> <aside> <a class="icon-btn" style="color: red" href="https://drops.dagstuhl.de/storage/00lipics/lipics-vol211-calco2021/LIPIcs.CALCO.2021.24/LIPIcs.CALCO.2021.24.pdf" data-bs-toggle="tooltip" title="View PDF"><i class="bi bi-file-earmark-pdf-fill"></i></a><a class="icon-btn" style="color: #0d6efd!important;" href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.24" data-bs-toggle="tooltip" title="View Detailed Metadata"><i class="bi bi-info-circle"></i></a><br/> <a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#abstract-15800" aria-expanded="false" aria-controls="collapseAbstract" title="Show Abstract"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show Abstract"><i class="bi bi-card-text"></i></span></a><a class="icon-btn investigation" href="#" data-bs-toggle="collapse" data-bs-target="#bibtex-15800" aria-expanded="false" aria-controls="collapseBibtex" title="Show BibTex"><span class="tooltip-wrapper" data-bs-toggle="tooltip" title="Show BibTex"><i class="bi bi-chat-left-quote"></i></a><br/><a class="icon-btn btn-statistics" data-entity="document/10.4230/LIPIcs.CALCO.2021.24" data-bs-toggle="tooltip" data-title="Minimality Notions via Factorization Systems ((Co)algebraic pearls)" href="#" title="Access Statistics"><i class="bi bi-graph-up"></i></a> </aside> <div class="selectors"> <span data-key="dagstuhl.contributor.author" data-value="Wißmann, Thorsten"></span> <span data-key="dagstuhl.subject.classification" data-value="Theory of computation → Formal languages and automata theory"></span> </div> <div class="card-body"> <h5 class="card-title"> <a href="https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.24"> Minimality Notions via Factorization Systems ((Co)algebraic pearls) </a> </h5> <p class="card-text small authors"> <b>Authors:</b> Thorsten Wißmann </p> <div class="row"> <div class="collapse" id="abstract-15800"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#abstract-15800">Abstract <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <div class="abstract monospace"> For the minimization of state-based systems (i.e. the reduction of the number of states while retaining the system’s semantics), there are two obvious aspects: removing unnecessary states of the system and merging redundant states in the system. In the present article, we relate the two aspects on coalgebras by defining an abstract notion of minimality. The abstract notion minimality and minimization live in a general category with a factorization system. We will find criteria on the category that ensure uniqueness, existence, and functoriality of the minimization aspects. The proofs of these results instantiate to those for reachability and observability minimization in the standard coalgebra literature. Finally, we will see how the two aspects of minimization interact and under which criteria they can be sequenced in any order, like in automata minimization. </div> </div> </div> <div class="row"> <div class="collapse" id="bibtex-15800"> <hr/> <h5 data-bs-toggle="collapse" data-bs-target="#bibtex-15800">Cite as <span style="float: right; cursor: pointer"><i class="bi bi-chevron-up"></i></span></h5> <p class="small">Thorsten Wißmann. Minimality Notions via Factorization Systems ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 24:1-24:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)</p> <hr/> <a href="#" class="btn btn-primary btn-xs copy-to-clipboard" title="Copy to clipboard" data-selector="bibtex-15800-input"><i class="bi bi-clipboard"></i> Copy BibTex To Clipboard<span class="bi bi-check -hidden" style="padding-left: 1em; font-weight: bold"></span></a><br/><br/> <pre class="bibtex">@InProceedings{wimann:LIPIcs.CALCO.2021.24, author = {Wi{\ss}mann, Thorsten}, title = {{Minimality Notions via Factorization Systems}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {24:1--24:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.24}, URN = {urn:nbn:de:0030-drops-153791}, doi = {10.4230/LIPIcs.CALCO.2021.24}, annote = {Keywords: Coalgebra, Reachability, Observability, Minimization, Factorization System} }</pre> <textarea style="position: absolute; top: 200vh" id="bibtex-15800-input">@InProceedings{wimann:LIPIcs.CALCO.2021.24, author = {Wi{\ss}mann, Thorsten}, title = {{Minimality Notions via Factorization Systems}}, booktitle = {9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)}, pages = {24:1--24:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-212-9}, ISSN = {1868-8969}, year = {2021}, volume = {211}, editor = {Gadducci, Fabio and Silva, Alexandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2021.24}, URN = {urn:nbn:de:0030-drops-153791}, doi = {10.4230/LIPIcs.CALCO.2021.24}, annote = {Keywords: Coalgebra, Reachability, Observability, Minimization, Factorization System} }</textarea> </div> </div> </div> </div> </div> </div> <div class="col-sm-3 mt-2"> <h2>Filters</h2> <div class="free-text-filter mb-4"> <div class="input-group"> <input class="form-control no-outline" type="search" placeholder="Free Text Filter" aria-label="Free Text Filter" id="free-text-filter" maxlength="300"> </div> </div> <div class="grouped-metadata-filter" data-filter-key="dagstuhl.contributor.author"> <ul class="list-group"> <li class="list-group-item filter-headline list-group-item-dark"> <b><span class="count"></span> Authors</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item filter-item pinned -hidden" data-value="" data-key=""> <i class="bi bi-pin-angle-fill"></i> <span class="value"></span> <span class="action"><i><i class="bi bi-x-circle"></i></i></span> </li> <li class="list-group-item details buttons"> <span class="btn-group" role="group" aria-label="Show-All/Collapse"> <button type="button" class="btn btn-primary">Show All</button> <button type="button" class="btn btn-secondary">Collapse</button> </span> </li> <li class="list-group-item details show-all -hidden"> <button type="button" class="btn btn-primary">Show All</button> </li> <li class="list-group-item details filter-group-headline -expanded " data-group-selector="dagstuhl.contributor.author.A"> <b>A</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value " data-key="dagstuhl.contributor.author" data-value="Adámek, Jiří" data-group-selector="dagstuhl.contributor.author.A"> Adámek, Jiří <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.B"> <b>B</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Bacci, Giorgio" data-group-selector="dagstuhl.contributor.author.B"> Bacci, Giorgio <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Baeten, Jos C. M." data-group-selector="dagstuhl.contributor.author.B"> Baeten, Jos C. M. <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Bonchi, Filippo" data-group-selector="dagstuhl.contributor.author.B"> Bonchi, Filippo <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.C"> <b>C</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Carissimo, Cesare" data-group-selector="dagstuhl.contributor.author.C"> Carissimo, Cesare <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Castelnovo, Davide" data-group-selector="dagstuhl.contributor.author.C"> Castelnovo, Davide <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Cheng, Eugenia" data-group-selector="dagstuhl.contributor.author.C"> Cheng, Eugenia <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.D"> <b>D</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Dahlqvist, Fredrik" data-group-selector="dagstuhl.contributor.author.D"> Dahlqvist, Fredrik <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="de Paiva, Valeria" data-group-selector="dagstuhl.contributor.author.D"> de Paiva, Valeria <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Di Giorgio, Alessandro" data-group-selector="dagstuhl.contributor.author.D"> Di Giorgio, Alessandro <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.F"> <b>F</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Ford, Chase" data-group-selector="dagstuhl.contributor.author.F"> Ford, Chase <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.G"> <b>G</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Gadducci, Fabio" data-group-selector="dagstuhl.contributor.author.G"> Gadducci, Fabio <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Garner, Richard" data-group-selector="dagstuhl.contributor.author.G"> Garner, Richard <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Giese, Holger" data-group-selector="dagstuhl.contributor.author.G"> Giese, Holger <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Grabmayer, Clemens" data-group-selector="dagstuhl.contributor.author.G"> Grabmayer, Clemens <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Gu, Tao" data-group-selector="dagstuhl.contributor.author.G"> Gu, Tao <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.J"> <b>J</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Jia, Xiaodong" data-group-selector="dagstuhl.contributor.author.J"> Jia, Xiaodong <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.L"> <b>L</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Lemay, Jean-Simon Pacaud" data-group-selector="dagstuhl.contributor.author.L"> Lemay, Jean-Simon Pacaud <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Luttik, Bas" data-group-selector="dagstuhl.contributor.author.L"> Luttik, Bas <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.M"> <b>M</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Mardare, Radu" data-group-selector="dagstuhl.contributor.author.M"> Mardare, Radu <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Master, Jade" data-group-selector="dagstuhl.contributor.author.M"> Master, Jade <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Miculan, Marino" data-group-selector="dagstuhl.contributor.author.M"> Miculan, Marino <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Milius, Stefan" data-group-selector="dagstuhl.contributor.author.M"> Milius, Stefan <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Mislove, Michael" data-group-selector="dagstuhl.contributor.author.M"> Mislove, Michael <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Moss, Lawrence S." data-group-selector="dagstuhl.contributor.author.M"> Moss, Lawrence S. <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Muroya, Koko" data-group-selector="dagstuhl.contributor.author.M"> Muroya, Koko <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.N"> <b>N</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Nakov, Georgi" data-group-selector="dagstuhl.contributor.author.N"> Nakov, Georgi <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Nordvall Forsberg, Fredrik" data-group-selector="dagstuhl.contributor.author.N"> Nordvall Forsberg, Fredrik <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.P"> <b>P</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Panangaden, Prakash" data-group-selector="dagstuhl.contributor.author.P"> Panangaden, Prakash <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Plotkin, Gordon" data-group-selector="dagstuhl.contributor.author.P"> Plotkin, Gordon <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.R"> <b>R</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Rosický, Jiří" data-group-selector="dagstuhl.contributor.author.R"> Rosický, Jiří <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.S"> <b>S</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Sanada, Takahiro" data-group-selector="dagstuhl.contributor.author.S"> Sanada, Takahiro <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Santamaria, Alessio" data-group-selector="dagstuhl.contributor.author.S"> Santamaria, Alessio <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Schmid, Todd" data-group-selector="dagstuhl.contributor.author.S"> Schmid, Todd <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Schröder, Lutz" data-group-selector="dagstuhl.contributor.author.S"> Schröder, Lutz <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Seeber, Jens" data-group-selector="dagstuhl.contributor.author.S"> Seeber, Jens <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Silva, Alexandra" data-group-selector="dagstuhl.contributor.author.S"> Silva, Alexandra <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Sobociński, Paweł" data-group-selector="dagstuhl.contributor.author.S"> Sobociński, Paweł <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Sokolova, Ana" data-group-selector="dagstuhl.contributor.author.S"> Sokolova, Ana <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.U"> <b>U</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Urabe, Natsuki" data-group-selector="dagstuhl.contributor.author.U"> Urabe, Natsuki <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.V"> <b>V</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Vafeiadis, Viktor" data-group-selector="dagstuhl.contributor.author.V"> Vafeiadis, Viktor <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Vignudelli, Valeria" data-group-selector="dagstuhl.contributor.author.V"> Vignudelli, Valeria <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.W"> <b>W</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Wißmann, Thorsten" data-group-selector="dagstuhl.contributor.author.W"> Wißmann, Thorsten <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Woracek, Harald" data-group-selector="dagstuhl.contributor.author.W"> Woracek, Harald <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.contributor.author.Z"> <b>Z</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Zamdzhiev, Vladimir" data-group-selector="dagstuhl.contributor.author.Z"> Zamdzhiev, Vladimir <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.contributor.author" data-value="Zanasi, Fabio" data-group-selector="dagstuhl.contributor.author.Z"> Zanasi, Fabio <span class="action"><i class="bi bi-plus-circle"></i></span> </li> </ul> </div> <br /> <div class="grouped-metadata-filter" data-filter-key="dagstuhl.subject.classification"> <ul class="list-group"> <li class="list-group-item filter-headline list-group-item-dark"> <b><span class="count"></span> Subjects</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item filter-item pinned -hidden" data-value="" data-key=""> <i class="bi bi-pin-angle-fill"></i> <span class="value"></span> <span class="action"><i><i class="bi bi-x-circle"></i></i></span> </li> <li class="list-group-item details buttons"> <span class="btn-group" role="group" aria-label="Show-All/Collapse"> <button type="button" class="btn btn-primary">Show All</button> <button type="button" class="btn btn-secondary">Collapse</button> </span> </li> <li class="list-group-item details show-all -hidden"> <button type="button" class="btn btn-primary">Show All</button> </li> <li class="list-group-item details filter-group-headline -expanded " data-group-selector="dagstuhl.subject.classification.Mathematics of computing"> <b>Mathematics of computing</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value " data-key="dagstuhl.subject.classification" data-value="Mathematics of computing → Mathematical analysis" data-group-selector="dagstuhl.subject.classification.Mathematics of computing"> Mathematics of computing → Mathematical analysis <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value " data-key="dagstuhl.subject.classification" data-value="Mathematics of computing → Probability and statistics" data-group-selector="dagstuhl.subject.classification.Mathematics of computing"> Mathematics of computing → Probability and statistics <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.subject.classification.Software and its engineering"> <b>Software and its engineering</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Software and its engineering → Context specific languages" data-group-selector="dagstuhl.subject.classification.Software and its engineering"> Software and its engineering → Context specific languages <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Software and its engineering → Software notations and tools" data-group-selector="dagstuhl.subject.classification.Software and its engineering"> Software and its engineering → Software notations and tools <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-group-headline " data-group-selector="dagstuhl.subject.classification.Theory of computation"> <b>Theory of computation</b> <span style="float: right;"><i class="bi bi-chevron-down"></i><i class="bi bi-chevron-up"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Algebraic language theory" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Algebraic language theory <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Algebraic semantics" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Algebraic semantics <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Automata over infinite objects" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Automata over infinite objects <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Axiomatic semantics" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Axiomatic semantics <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Categorical semantics" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Categorical semantics <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Denotational semantics" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Denotational semantics <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Design and analysis of algorithms" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Design and analysis of algorithms <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Equational logic and rewriting" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Equational logic and rewriting <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Formal languages and automata theory" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Formal languages and automata theory <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Grammars and context-free languages" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Grammars and context-free languages <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Interactive computation" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Interactive computation <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Linear logic" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Linear logic <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Logic" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Logic <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Logic and verification" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Logic and verification <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Modal and temporal logics" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Modal and temporal logics <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Models of computation" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Models of computation <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Operational semantics" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Operational semantics <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Process calculi" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Process calculi <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Program specifications" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Program specifications <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Quantum computation theory" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Quantum computation theory <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Semantics and reasoning" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Semantics and reasoning <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Turing machines" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Turing machines <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Type theory" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Type theory <span class="action"><i class="bi bi-plus-circle"></i></span> </li> <li class="list-group-item details filter-item value -hidden " data-key="dagstuhl.subject.classification" data-value="Theory of computation → Verification by model checking" data-group-selector="dagstuhl.subject.classification.Theory of computation"> Theory of computation → Verification by model checking <span class="action"><i class="bi bi-plus-circle"></i></span> </li> </ul> </div> </div> </div> <div class="offcanvas offcanvas-bottom" tabindex="-1" id="statistics-offcanvas" aria-labelledby="statistics-offcanvas"> <div class="offcanvas-header"> <h5 class="offcanvas-title"></h5> <button type="button" class="btn-close text-reset" data-bs-dismiss="offcanvas" aria-label="Close"></button> </div> <div class="offcanvas-body small" data-context="9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)"> <div style="margin-top: 20vh" class="centered-loader"><div class="loader"></div></div> <iframe class="-hidden"></iframe> </div> </div> </div> </div> <span class="_feedback-button"> <i class="bi bi-question-circle"></i> <span class="text">Questions / Remarks / Feedback</span> </span> <div class="_feedback-form -hidden"> <span class="_feedback-close">X</span> <p>Feedback for Dagstuhl Publishing</p> <div> <textarea class="form-control" name="_feedback"></textarea> <input class="form-control" type="text" name="name" autocomplete="off" placeholder="Name (optional)" maxlength="60" /> <input class="form-control" type="email" name="email" autocomplete="off" placeholder="Email (optional)" maxlength="60" /> <br/> <button class="btn btn-sm btn-default">Send</button> </div> </div> <div class="alert alert-success _feedback-success -hidden"> <span class="glyphicon glyphicon-ok"></span> <h3>Thanks for your feedback!</h3> <div>Feedback submitted</div> <button class="btn btn-white _feedback-done">OK</button> </div> <div class="alert alert-danger _feedback-error -hidden"> <span class="glyphicon glyphicon-remove"></span> <h3>Could not send message</h3> <div>Please try again later or send an <a href="mailto:publishing@dagstuhl.de">E-mail</a></div> <button class="btn btn-white _feedback-done">OK</button> </div> <a class="scroll-up-button -hidden" href="#_top-of-page"> <i class="bi bi-arrow-up-circle"></i> </a> <footer class="page-footer dark"> <div class="container"> <h5>About DROPS</h5> <p>Schloss Dagstuhl - Leibniz Center for Informatics has been operating the Dagstuhl Research Online Publication Server (short: DROPS) since 2004. DROPS enables publication of the latest research findings in a fast, uncomplicated manner, in addition to providing unimpeded, open access to them. All the requisite metadata on each publication is administered in accordance with general guidelines pertaining to online publications (cf. Dublin Core). This enables the online publications to be authorized for citation and made accessible to a wide readership on a permanent basis. Access is free of charge for readers following the open access idea which fosters unimpeded access to scientific publications. </p> </div> <div class="container"> <div class="row"> <div class="col-lg-6"> <h5>Instructions for Authors</h5> <div class="row"> <div class="col-sm-6"> <b>Dagstuhl Series</b><br> <ul> <li><a href="https://submission.dagstuhl.de/series/details/lipics#author">LIPIcs</a></li> <li><a href="https://submission.dagstuhl.de/series/details/oasics#author">OASIcs</a></li> <li><a href="https://submission.dagstuhl.de/series/details/dfu#author">Dagstuhl Follow-Ups</a></li> </ul> </div> <div class="col-sm-6"> <b>Dagstuhl Journals</b><br> <ul> <li><a href="https://submission.dagstuhl.de/series/details/darts#author">DARTS – Dagstuhl Artifacts Series</a></li> <li><a href="https://submission.dagstuhl.de/series/details/dagrep#author">Dagstuhl Reports</a></li> <li><a href="https://submission.dagstuhl.de/series/details/dagman#author">Dagstuhl Manifestos</a></li> <li><a href="https://submission.dagstuhl.de/series/details/lites#author">LITES</a></li> <li><a href="https://submission.dagstuhl.de/series/details/tgdk#author">TGDK – Transactions on Graph Data and Knowledge</a></li> </ul> </div> </div> </div> <div class="col-lg-6"> <h5>Instructions for Editors</h5> <div class="row"> <div class="col-sm-6"> <b>Dagstuhl Series</b><br> <ul> <li><a href="https://submission.dagstuhl.de/series/details/lipics#editor">LIPIcs</a></li> <li><a href="https://submission.dagstuhl.de/series/details/oasics#editor">OASIcs</a></li> <li><a href="https://submission.dagstuhl.de/series/details/dfu#editor">Dagstuhl Follow-Ups</a></li> </ul> </div> <div class="col-sm-6"> <b>Dagstuhl Journals</b><br> <ul> <li><a href="https://submission.dagstuhl.de/series/details/darts#editor">DARTS – Dagstuhl Artifacts Series</a></li> <li><a href="https://submission.dagstuhl.de/series/details/dagrep#editor">Dagstuhl Reports</a></li> <li><a href="https://submission.dagstuhl.de/series/details/dagman#editor">Dagstuhl Manifestos</a></li> <li><a href="https://submission.dagstuhl.de/series/details/lites#editor">LITES</a></li> <li><a href="https://submission.dagstuhl.de/series/details/tgdk#editor">TGDK – Transactions on Graph Data and Knowledge</a></li> </ul> </div> </div> </div> </div> </div> </footer> <div class="copyright"> © 2023-2024 <a href="https://www.dagstuhl.de">Schloss Dagstuhl – LZI GmbH</a> <a href="https://drops.dagstuhl.de/docs/imprint">Imprint</a> <a href="https://drops.dagstuhl.de/docs/privacy">Privacy</a> <a href="https://www.dagstuhl.de/en/publishing/team">Contact</a> </div> <script type="text/javascript" src="https://drops.dagstuhl.de/js/jquery-3.6.0.min.js"></script> <script type="text/javascript" src="https://drops.dagstuhl.de/js/app.js?drops-core-2024-10-22"></script> <script type="text/javascript" src="https://drops.dagstuhl.de/js/popper.min.js"></script> <script type="text/javascript" src="https://drops.dagstuhl.de/js/circle-progress.js"></script> <script type="text/javascript"> $(document).ready(function() { const view = { statsServer: 'https://drops-stats.dagstuhl.de', animationStarted: false, isScrolledIntoView: function (elem) { const rect = elem.getBoundingClientRect(); const elemTop = rect.top; //const elemBottom = rect.bottom; // const elemHeight = rect.height; return (elemTop >= 0) && (elemTop <= window.innerHeight); }, progressCircle: function ($el) { $el.find('.circle').circleProgress({ value: 1, size: 80, fill: { color: '#555' }, animation: { duration: 1200 } }); }, countUp: function($el) { $el.find('.number').each(function() { const $this = $(this); const number = parseInt($this.attr('data-number')); let suffix = ''; if (number > 90000) { $this.text(Math.ceil(number/1000)+' k'); suffix = ' k'; } else if (number > 90000000) { $this.text(Math.ceil(number/1000000)+' m'); suffix = ' m'; } else { $this.text(Math.ceil(number)) } $({ Counter: 0 }).animate({ Counter: $this.text().replace(suffix, '').replace(',', '') }, { duration: 1000, easing: 'swing', step: function() { $this.text(Math.ceil(this.Counter).toString().replace(/\B(?=(\d{3})+(?!\d))/g, ",") + suffix); } }); }); }, checkVisibility: function() { const $container = $('.stats-total'); if (view.isScrolledIntoView($container[0])) { if (!view.animationStarted) { view.animationStarted = true; view.progressCircle($container); setTimeout(function() { view.countUp($container) }, 200); } } }, initialize: function() { $.ajax({ type: 'get', url: view.statsServer + '/api/external/drops2/volume/LIPIcs-volume-211/-/stats', success: function (result) { $('.total-downloads .number').attr('data-number', result.total.downloads); $('.total-metadata-views .number').attr('data-number', result.total.clicks); window.addEventListener('scroll', view.checkVisibility); view.checkVisibility(); }, error: function () { $('.total-downloads .number').text(0); $('.total-metadata-views .number').text(0); window.addEventListener('scroll', view.checkVisibility); view.checkVisibility(); } }); } }; view.initialize(); }); </script> <script type="text/javascript"> $(document).ready(function() { const view = { trackInvestigation: function(e) { const $entity = $(e.currentTarget).parent().parent(); const permanentId = $entity.attr('data-permanent-id'); $.ajax({ url: '/entities/' + permanentId + '/_investigation', type: 'get', }); }, initialize: function() { $('a.investigation').on('click', view.trackInvestigation); } }; view.initialize(); }); </script> <script type="text/javascript"> $(document).ready(function() { const view = { $el: { root: $('.grouped-metadata-filter'), freeTextFilter: $('#free-text-filter') }, appliedFilters: { freeText: [] }, methods: { toggleDetails: function(e) { var $current = $(e.currentTarget); var $parent = $current.parent(); $parent.toggleClass('-expanded'); }, toggleGroup: function(e) { var $current = $(e.currentTarget); var selector = $current.attr('data-group-selector'); $current.toggleClass('-expanded'); $('.filter-item[data-group-selector="' + selector + '"]').toggleClass('-hidden'); }, toggleFilter: function(e) { var $current = $(e.currentTarget); var key = $current.attr('data-key'); var value = $current.attr('data-value'); if (view.appliedFilters[key] === undefined) { view.appliedFilters[key] = []; } var index = view.appliedFilters[key].indexOf(value); if (index !== -1) { view.appliedFilters[key].splice(index, 1); $('.grouped-metadata-filter[data-filter-key="'+key+'"]').find('.pinned[data-value="'+value+'"]').remove(); } else { view.appliedFilters[key].push(value); var $template = $('.grouped-metadata-filter[data-filter-key="'+key+'"]').find('.pinned.-hidden'); var $filter = $template.clone(); $filter.find('.value').html(value); $filter.attr('data-value', value) .attr('data-key', key) .removeClass('-hidden') .insertAfter($template) .on('click', view.methods.toggleFilter); } var event = (index !== -1) ? 'removeFilter' : 'addFilter'; var filterCount = 0; for(var filterKey in view.appliedFilters) { filterCount += view.appliedFilters[filterKey].length; } $(document).trigger('grouped-metadata-filter:' + event, { key: key, value: value, appliedFilters: view.appliedFilters, filterCount: filterCount }); }, setFreeTextFilter: function(e) { var $current = $(e.currentTarget); var value = $current.val().trim(); if (value === '') { view.appliedFilters.freeText = [] } else { view.appliedFilters.freeText = [ value ]; } var filterCount = 0; for(var filterKey in view.appliedFilters) { filterCount += view.appliedFilters[filterKey].length; } $(document).trigger('grouped-metadata-filter:addFilter', { key: 'free-text', value: value, appliedFilters: view.appliedFilters, filterCount: filterCount }); }, dropAllFilters: function() { $('.grouped-metadata-filter').find('.filter-item.pinned:not(.-hidden)').click(); $('#free-text-filter').val('').trigger('keyup'); }, expandAllGroups: function(e) { var $current = $(e.currentTarget); $current.parent().parent().parent().find('.filter-group-headline:not(.-expanded)').click(); }, collapseAllGroups: function(e) { var $current = $(e.currentTarget); var $filter = $current.parent().parent().parent(); $filter.find('.filter-group-headline.-expanded').click(); $filter.find('.filter-headline').click(); $filter.find('.filter-headline').click(); } }, initialize: function() { view.$el.root.each(function() { var count = $(this).find('.filter-item.value').length; $(this).find('.filter-headline .count').text(count); }); view.$el.root.find('.filter-group-headline').on('click', view.methods.toggleGroup); view.$el.root.find('.filter-item').on('click', view.methods.toggleFilter); view.$el.root.find('.filter-headline').on('click', view.methods.toggleDetails); view.$el.root.find('.buttons .btn-primary').on('click', view.methods.expandAllGroups); view.$el.root.find('.buttons .btn-secondary').on('click', view.methods.collapseAllGroups); view.$el.freeTextFilter.on('keyup', view.methods.setFreeTextFilter); view.$el.freeTextFilter.on('search', view.methods.setFreeTextFilter); $(document).on('grouped-metadata-filter:dropAllFilters', view.methods.dropAllFilters); } }; view.initialize(); }); </script> <script type="text/javascript"> $(document).ready(function() { const view = { normalize: function(string) { return string.normalize('NFD').replace(/[\u0300-\u036f]/g, ""); }, applyFilters: function(e, data) { var $documents = $('.document'); var $noResults = $('.no-results'); $documents.each(function() { var $document = $(this); var matches = 0; for(var filterKey in data.appliedFilters) { var values = data.appliedFilters[filterKey]; if (filterKey === 'freeText' && values[0] !== undefined && values[0] !== '') { var regex = new RegExp(view.normalize(values[0].toLowerCase()), 'i'); matches += view.normalize($document.html()).match(regex) ? 1 : 0; } else { values.forEach(function (value) { matches += $document.find('.selectors').find('[data-key="' + filterKey + '"][data-value="' + value + '"]').length }); } } if (matches === data.filterCount) { $document.removeClass('-hidden'); } else { $document.addClass('-hidden') } }); if ($documents.parent().find('.document:not(.-hidden').length === 0) { $noResults.removeClass('-hidden'); } else { $noResults.addClass('-hidden'); } document.getElementById('end-of-header').scrollIntoView(); var filterInfo = ''; if (data.filterCount === 1) { filterInfo = '1 filter applied   ×'; } else if (data.filterCount > 1) { filterInfo = data.filterCount + ' filters applied   ×'; } $('._filter-info').html(filterInfo); if (data.appliedFilters.freeText[0] !== undefined && data.appliedFilters.freeText[0] !== '') { $('#free-text-filter').addClass('-active'); } else { $('#free-text-filter').removeClass('-active'); } }, initialize: function() { $(document).on('grouped-metadata-filter:addFilter', view.applyFilters); $(document).on('grouped-metadata-filter:removeFilter', view.applyFilters); } }; view.initialize(); }); </script> <script type="text/javascript"> function _enableFeedback() { var $feedbackButton = $('._feedback-button, .fixed-beta-button'); var $feedbackClose = $('._feedback-close'); var $feedbackForm = $('._feedback-form'); var $feedbackSubmit = $('._feedback-form button'); var $textarea = $feedbackForm.find('textarea'); var $feedbackSuccess = $('._feedback-success'); var $feedbackError = $('._feedback-error'); var $feedbackDoneButton = $('._feedback-done'); $feedbackButton.addClass('_show'); $feedbackButton.on('click', function () { $feedbackButton.addClass('-hidden'); $feedbackForm.removeClass('-hidden'); $textarea.focus(); }); $feedbackClose.on('click', function () { $feedbackSuccess.addClass('-hidden'); $feedbackForm.addClass('-hidden'); $feedbackButton.removeClass('-hidden'); }); $feedbackDoneButton.on('click', function () { $feedbackError.addClass('-hidden'); $feedbackSuccess.addClass('-hidden'); $feedbackForm.addClass('-hidden'); $feedbackButton.removeClass('-hidden'); }); $feedbackSubmit.on('click', function () { var message = $textarea.val(); if (message === undefined) { message = ''; } if (message.trim() !== '') { $.ajax({ url: '/api/v1/feedback', type: 'post', data: { content: message, context: window.location.href, name: $('input[name="name"]').val(), email: $('input[name="email"]').val(), }, success: function (result) { if (result === 'success') { $textarea.val(''); $feedbackSuccess.removeClass('-hidden'); } else { $feedbackError.removeClass('-hidden'); } }, error: function () { $feedbackError.removeClass('-hidden'); } }); } }); } var _defer_counter = 0; function _defer(method) { if (window.jQuery) { method(); } else { if (_defer_counter < 20) { setTimeout(function () { _defer(method); console.log(_defer_counter); _defer_counter++; }, 500); } } } setTimeout(function() { _defer(_enableFeedback); }, 1000); </script> <script type="text/javascript"> $(document).ready(function() { $('._filter-info').on('click', function() { $(document).trigger('grouped-metadata-filter:dropAllFilters'); }); }); </script> <script type="text/javascript"> $(document).ready(function() { const statistics = { statsServer: 'https://drops-stats.dagstuhl.de', showStatistics: function(e) { e.preventDefault(); const $offCanvas = $('#statistics-offcanvas'); const $iframe = $offCanvas.find('iframe'); const $loader = $offCanvas.find('.centered-loader'); $iframe.addClass('-hidden'); $loader.removeClass('-hidden'); $iframe[0].onload = function () { $iframe.removeClass('-hidden'); $loader.addClass('-hidden'); }.bind(this); const modeParameter = ''; const $target = $(e.currentTarget); const entityId = $target.attr('data-entity'); const title = $target.attr('data-title'); const embedUrl = statistics.statsServer + '/embed/external/drops2/' + entityId + modeParameter; let context = $offCanvas.find('.offcanvas-body').attr('data-context'); if (context === title) { context = ''; } if (context !== '') { context += '<br>'; } $offCanvas.find('.offcanvas-title').html(context + '<h2 style="font-weight: bold">' + title + '</h2>'); $offCanvas.offcanvas('show'); $offCanvas.find('iframe').attr('src', embedUrl); return false; }, initialize: function() { $('.btn-statistics').on('click', this.showStatistics); } }; statistics.initialize(); }); </script> <script type="text/javascript"> $(document).ready(function() { const app = { maxScrollPos: window.innerWidth < 500 ? 100 // mobile : 400, // desktop $el : { navbarSearch: $('nav .navbar-search'), fixedSearchButton: $('.fixed-search-button'), copyToClipboard: $('.copy-to-clipboard') }, methods: { hideMenuOnScroll: function(scrollPos) { const $menu = $('nav.navbar.main'); const $stickySearch = $('.search.sticky'); const $banner = $('#_banner'); const $fixedSearchButton = $('.fixed-search-button'); if (scrollPos > app.maxScrollPos) { $menu.addClass('-hide'); $banner.addClass('-hide'); $stickySearch.addClass('-top'); $fixedSearchButton.addClass('-show'); } else { app.methods.showMenu(null, false); } }, showMenu: function(e, focus) { const $menu = $('nav.navbar.main'); const $stickySearch = $('.search.sticky'); const $banner = $('#_banner'); const $fixedSearchButton = $('.fixed-search-button'); $menu.removeClass('-hide'); $banner.removeClass('-hide'); $stickySearch.removeClass('-top'); $fixedSearchButton.removeClass('-show'); if (focus !== false) { $('.navbar-search').find('input[name="term"]').focus(); } }, showUpLinkOnScroll: function(scrollPos) { const $upLink = $('.scroll-up-button'); if (scrollPos > app.maxScrollPos) { $upLink.removeClass('-hidden'); } else { $upLink.addClass('-hidden'); } }, scrollHandler: function() { const scrollPos = $(document).scrollTop(); app.methods.hideMenuOnScroll(scrollPos); app.methods.showUpLinkOnScroll(scrollPos); }, copyToClipboard: function(e) { e.preventDefault(); const $current = $(e.currentTarget); // console.log($current.attr('data-selector')); const element = $('#'+$current.attr('data-selector'))[0]; console.log(element); element.select(); document.execCommand("copy"); const $success = $current.find('.bi-check'); $success.removeClass('-hidden'); setTimeout(function() { $success.addClass('-hidden'); }, 1000); }, initTooltips: function() { const tooltipTriggerList = [].slice.call(document.querySelectorAll('[data-bs-toggle="tooltip"]')) const tooltipList = tooltipTriggerList.map(function (tooltipTriggerEl) { return new bootstrap.Tooltip(tooltipTriggerEl) }); }, expandSearch: function() { app.$el.navbarSearch.addClass('expanded'); }, collapseSearch: function(e) { if (!$(e.currentTarget).is('button.btn-outline-success')) { app.$el.navbarSearch.removeClass('expanded'); } }, initDeepLinksTabs: function() { const innerAnchors = [ 'resource-articles', 'cfp-si-resources', 'cfp-si-autonomous-systems-and-knowledge-graphs' ]; let anchors = []; $('a[role="tab"]').each(function() { anchors.push($(this).attr('aria-controls')); }); innerAnchors.forEach(function(anchor) { if ($('#'+anchor).length > 0) { anchors.push(anchor); } }); if (anchors.length === 0) { return; } let selectedAnchor = window.location.hash.substring(1); if (anchors.indexOf(selectedAnchor) === -1) { $('#publications-tab').tab('show'); window.scrollTo(0,0); return; } if (selectedAnchor !== 'publications') { const innerAnchorIndex = innerAnchors.indexOf(selectedAnchor); // anchor sits inside tab -> open the tab first, then scroll to anchor if (innerAnchorIndex > -1) { const $tab = $('#'+selectedAnchor).closest('.tab-pane'); console.log($tab); try { $('#'+$tab.attr('id')+'-tab').tab('show'); } catch (e) { } setTimeout(function () { $('#' + selectedAnchor)[0].scrollIntoView(); }, 800); } else { try { $('#' + selectedAnchor + '-tab').tab('show'); } catch (e) { } window.scrollTo(0, 0); } } $('[data-tab-link]').on('click', function(e) { const $target = $(e.currentTarget); let href = $target.attr('href'); let scrollLink = null; if (href === '#cfp-si-list') { scrollLink = href; href = '#cfp'; } try { console.log(href); $(href+'-tab').tab('show'); } catch(e) { } console.log(scrollLink); if (scrollLink !== null) { setTimeout(function() { $(scrollLink)[0].scrollIntoView(); }, 200); } else { setTimeout(function() { window.scrollTo(0,0); }, 200); } }); } }, initialize: function() { $(window).on('scroll', app.methods.scrollHandler); $(window).on('scroll-to-top', function() { window.scrollTo(0,0) }); $(document).trigger('scroll'); // set correct status for scroll-related parts (navbar/back-to-top) on page reload app.$el.copyToClipboard.on('click', app.methods.copyToClipboard); app.$el.fixedSearchButton.on('click', app.methods.showMenu); app.$el.navbarSearch.find('input').on('click', app.methods.expandSearch) app.$el.navbarSearch.find('input').on('blur', app.methods.collapseSearch); app.methods.initTooltips(); app.methods.initDeepLinksTabs(); } }; app.initialize(); }); </script> </body> </html>

CINXE.COM

9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021)