Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Sam Ezeh. Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4 (Short Paper). In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 41:1-41:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{ezeh:LIPIcs.ITP.2024.41, author = {Ezeh, Sam}, title = {{Graphical Rewriting for Diagrammatic Reasoning in Monoidal Categories in Lean4}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {41:1--41:8}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-337-9}, ISSN = {1868-8969}, year = {2024}, volume = {309}, editor = {Bertot, Yves and Kutsia, Temur and Norrish, Michael}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.41}, URN = {urn:nbn:de:0030-drops-207690}, doi = {10.4230/LIPIcs.ITP.2024.41}, annote = {Keywords: Interactive theorem proving, Lean4, Graphical User Interface} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Sergey Goncharov and Tarmo Uustalu. A Unifying Categorical View of Nondeterministic Iteration and Tests. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 25:1-25:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{goncharov_et_al:LIPIcs.CONCUR.2024.25, author = {Goncharov, Sergey and Uustalu, Tarmo}, title = {{A Unifying Categorical View of Nondeterministic Iteration and Tests}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {25:1--25:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-339-3}, ISSN = {1868-8969}, year = {2024}, volume = {311}, editor = {Majumdar, Rupak 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.CONCUR.2024.25}, URN = {urn:nbn:de:0030-drops-207979}, doi = {10.4230/LIPIcs.CONCUR.2024.25}, annote = {Keywords: Kleene iteration, Elgot iteration, Kleene algebra, coalgebraic resumptions} }
Published in: LIPIcs, Volume 306, 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)
Niel de Beaudrap and Richard D. P. East. Simple Qudit ZX and ZH Calculi, via Integrals. In 49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 306, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{debeaudrap_et_al:LIPIcs.MFCS.2024.20, author = {de Beaudrap, Niel and East, Richard D. P.}, title = {{Simple Qudit ZX and ZH Calculi, via Integrals}}, booktitle = {49th International Symposium on Mathematical Foundations of Computer Science (MFCS 2024)}, pages = {20:1--20:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-335-5}, ISSN = {1868-8969}, year = {2024}, volume = {306}, editor = {Kr\'{a}lovi\v{c}, Rastislav and Ku\v{c}era, Anton{\'\i}n}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2024.20}, URN = {urn:nbn:de:0030-drops-205761}, doi = {10.4230/LIPIcs.MFCS.2024.20}, annote = {Keywords: ZX-calculus, ZH-calculus, qudits, string diagrams, discrete integrals} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Benoît Guillemet, Assia Mahboubi, and Matthieu Piquerez. Machine-Checked Categorical Diagrammatic Reasoning. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{guillemet_et_al:LIPIcs.FSCD.2024.7, author = {Guillemet, Beno\^{i}t and Mahboubi, Assia and Piquerez, Matthieu}, title = {{Machine-Checked Categorical Diagrammatic Reasoning}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {7:1--7:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.7}, URN = {urn:nbn:de:0030-drops-203363}, doi = {10.4230/LIPIcs.FSCD.2024.7}, annote = {Keywords: Interactive theorem proving, categories, diagrams, formal proof automation} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Maximilian Doré, Evan Cavallo, and Anders Mörtberg. Automating Boundary Filling in Cubical Agda. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{dore_et_al:LIPIcs.FSCD.2024.22, author = {Dor\'{e}, Maximilian and Cavallo, Evan and M\"{o}rtberg, Anders}, title = {{Automating Boundary Filling in Cubical Agda}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {22:1--22:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.22}, URN = {urn:nbn:de:0030-drops-203514}, doi = {10.4230/LIPIcs.FSCD.2024.22}, annote = {Keywords: Cubical Agda, Automated Reasoning, Constraint Satisfaction Programming} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Nathan Corbyn, Lukas Heidemann, Nick Hu, Chiara Sarti, Calin Tataru, and Jamie Vicary. homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 30:1-30:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{corbyn_et_al:LIPIcs.FSCD.2024.30, author = {Corbyn, Nathan and Heidemann, Lukas and Hu, Nick and Sarti, Chiara and Tataru, Calin and Vicary, Jamie}, title = {{homotopy.io: A Proof Assistant for Finitely-Presented Globular n-Categories}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {30:1--30:26}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-323-2}, ISSN = {1868-8969}, year = {2024}, volume = {299}, editor = {Rehof, Jakob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.30}, URN = {urn:nbn:de:0030-drops-203594}, doi = {10.4230/LIPIcs.FSCD.2024.30}, annote = {Keywords: Higher category theory, proof assistant, string diagrams} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Jonathan Sterling and Robert Harper. Sheaf Semantics of Termination-Insensitive Noninterference. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{sterling_et_al:LIPIcs.FSCD.2022.5, author = {Sterling, Jonathan and Harper, Robert}, title = {{Sheaf Semantics of Termination-Insensitive Noninterference}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {5:1--5:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-233-4}, ISSN = {1868-8969}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.5}, URN = {urn:nbn:de:0030-drops-162869}, doi = {10.4230/LIPIcs.FSCD.2022.5}, annote = {Keywords: information flow, noninterference, denotational semantics, phase distinction, Artin gluing, modal type theory, topos theory, synthetic domain theory, synthetic Tait computability} }
Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)
David Reutter and Jamie Vicary. A Classical Groupoid Model for Quantum Networks. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{reutter_et_al:LIPIcs.CALCO.2017.19, author = {Reutter, David and Vicary, Jamie}, title = {{A Classical Groupoid Model for Quantum Networks}}, booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)}, pages = {19:1--19:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-033-0}, ISSN = {1868-8969}, year = {2017}, volume = {72}, editor = {Bonchi, Filippo and K\"{o}nig, Barbara}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.19}, URN = {urn:nbn:de:0030-drops-80391}, doi = {10.4230/LIPIcs.CALCO.2017.19}, annote = {Keywords: groupoids, networks, quantum, semantics, key distribution} }
Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)
David Reutter and Jamie Vicary. A 2-Categorical Approach to Composing Quantum Structures. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
@InProceedings{reutter_et_al:LIPIcs.CALCO.2017.20, author = {Reutter, David and Vicary, Jamie}, title = {{A 2-Categorical Approach to Composing Quantum Structures}}, booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)}, pages = {20:1--20:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-033-0}, ISSN = {1868-8969}, year = {2017}, volume = {72}, editor = {Bonchi, Filippo and K\"{o}nig, Barbara}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.20}, URN = {urn:nbn:de:0030-drops-80389}, doi = {10.4230/LIPIcs.CALCO.2017.20}, annote = {Keywords: quantum constructions, 2-category, graphical calculus, planar algebra} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Krzysztof Bar, Aleks Kissinger, and Jamie Vicary. Globular: An Online Proof Assistant for Higher-Dimensional Rewriting. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 34:1-34:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{bar_et_al:LIPIcs.FSCD.2016.34, author = {Bar, Krzysztof and Kissinger, Aleks and Vicary, Jamie}, title = {{Globular: An Online Proof Assistant for Higher-Dimensional Rewriting}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {34:1--34:11}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-010-1}, ISSN = {1868-8969}, year = {2016}, volume = {52}, editor = {Kesner, Delia and Pientka, Brigitte}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.34}, URN = {urn:nbn:de:0030-drops-59880}, doi = {10.4230/LIPIcs.FSCD.2016.34}, annote = {Keywords: higher category theory, higher-dimensional rewriting, interactive theorem proving} }
Feedback for Dagstuhl Publishing