Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Henning Basold, Peter Bruin, and Dominique Lawson. The Directed Van Kampen Theorem in Lean. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{basold_et_al:LIPIcs.ITP.2024.8, author = {Basold, Henning and Bruin, Peter and Lawson, Dominique}, title = {{The Directed Van Kampen Theorem in Lean}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {8:1--8:18}, 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.8}, URN = {urn:nbn:de:0030-drops-207368}, doi = {10.4230/LIPIcs.ITP.2024.8}, annote = {Keywords: Lean, Directed Topology, Van Kampen Theorem, Directed Homotopy Theory, Formalised Mathematics} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Camil Champin, Samuel Mimram, and Émile Oleon. Delooping Generated Groups in Homotopy Type Theory. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{champin_et_al:LIPIcs.FSCD.2024.6, author = {Champin, Camil and Mimram, Samuel and Oleon, \'{E}mile}, title = {{Delooping Generated Groups in Homotopy Type Theory}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {6:1--6:20}, 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.6}, URN = {urn:nbn:de:0030-drops-203356}, doi = {10.4230/LIPIcs.FSCD.2024.6}, annote = {Keywords: homotopy type theory, delooping, group, generator, Cayley graph} }
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 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Samuel Mimram. Categorical Coherence from Term Rewriting Systems. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{mimram:LIPIcs.FSCD.2023.16, author = {Mimram, Samuel}, title = {{Categorical Coherence from Term Rewriting Systems}}, booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)}, pages = {16:1--16:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-277-8}, ISSN = {1868-8969}, year = {2023}, volume = {260}, editor = {Gaboardi, Marco and van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.16}, URN = {urn:nbn:de:0030-drops-180009}, doi = {10.4230/LIPIcs.FSCD.2023.16}, annote = {Keywords: coherence, rewriting system, Lawvere theory} }
Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)
Thibaut Benjamin. Formalisation of Dependent Type Theory: The Example of CaTT. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{benjamin:LIPIcs.TYPES.2021.2, author = {Benjamin, Thibaut}, title = {{Formalisation of Dependent Type Theory: The Example of CaTT}}, booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)}, pages = {2:1--2:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-254-9}, ISSN = {1868-8969}, year = {2022}, volume = {239}, editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.2}, URN = {urn:nbn:de:0030-drops-167719}, doi = {10.4230/LIPIcs.TYPES.2021.2}, annote = {Keywords: Dependent type theory, homotopy type theory, higher categories, formalisation, Agda, proof assistant} }
Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Samuel Mimram and Émile Oleon. Division by Two, in Homotopy Type Theory. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{mimram_et_al:LIPIcs.FSCD.2022.11, author = {Mimram, Samuel and Oleon, \'{E}mile}, title = {{Division by Two, in Homotopy Type Theory}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {11:1--11:17}, 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.11}, URN = {urn:nbn:de:0030-drops-162920}, doi = {10.4230/LIPIcs.FSCD.2022.11}, annote = {Keywords: division, axiom of choice, set theory, homotopy type theory, Agda} }
Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)
Samuel Balco and Alexander Kurz. Nominal String Diagrams. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{balco_et_al:LIPIcs.CALCO.2019.18, author = {Balco, Samuel and Kurz, Alexander}, title = {{Nominal String Diagrams}}, booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)}, pages = {18:1--18:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-120-7}, ISSN = {1868-8969}, year = {2019}, volume = {139}, editor = {Roggenbach, Markus and Sokolova, Ana}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.18}, URN = {urn:nbn:de:0030-drops-114466}, doi = {10.4230/LIPIcs.CALCO.2019.18}, annote = {Keywords: string diagrams, nominal sets, separated product, simultaneous substitutions, internal category, monoidal category, internal monoidal categories, PROP} }
Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)
Jérémy Ledent and Samuel Mimram. A Sound Foundation for the Topological Approach to Task Solvability. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{ledent_et_al:LIPIcs.CONCUR.2019.34, author = {Ledent, J\'{e}r\'{e}my and Mimram, Samuel}, title = {{A Sound Foundation for the Topological Approach to Task Solvability}}, booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)}, pages = {34:1--34:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-121-4}, ISSN = {1868-8969}, year = {2019}, volume = {140}, editor = {Fokkink, Wan and van Glabbeek, Rob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.34}, URN = {urn:nbn:de:0030-drops-109365}, doi = {10.4230/LIPIcs.CONCUR.2019.34}, annote = {Keywords: Fault-tolerant protocols, Asynchronous computability, Combinatorial topology, Protocol complex, Distributed task} }
Published in: LIPIcs, Volume 125, 22nd International Conference on Principles of Distributed Systems (OPODIS 2018)
Éric Goubault, Jérémy Ledent, and Samuel Mimram. Concurrent Specifications Beyond Linearizability. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{goubault_et_al:LIPIcs.OPODIS.2018.28, author = {Goubault, \'{E}ric and Ledent, J\'{e}r\'{e}my and Mimram, Samuel}, title = {{Concurrent Specifications Beyond Linearizability}}, booktitle = {22nd International Conference on Principles of Distributed Systems (OPODIS 2018)}, pages = {28:1--28:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-098-9}, ISSN = {1868-8969}, year = {2019}, volume = {125}, editor = {Cao, Jiannong and Ellen, Faith and Rodrigues, Luis and Ferreira, Bernardo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2018.28}, URN = {urn:nbn:de:0030-drops-100888}, doi = {10.4230/LIPIcs.OPODIS.2018.28}, annote = {Keywords: concurrent specification, concurrent object, linearizability} }
Published in: LIPIcs, Volume 121, 32nd International Symposium on Distributed Computing (DISC 2018)
Éric Goubault, Jérémy Ledent, and Samuel Mimram. Brief Announcement: On the Impossibility of Detecting Concurrency. In 32nd International Symposium on Distributed Computing (DISC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 121, pp. 50:1-50:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{goubault_et_al:LIPIcs.DISC.2018.50, author = {Goubault, \'{E}ric and Ledent, J\'{e}r\'{e}my and Mimram, Samuel}, title = {{Brief Announcement: On the Impossibility of Detecting Concurrency}}, booktitle = {32nd International Symposium on Distributed Computing (DISC 2018)}, pages = {50:1--50:4}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-092-7}, ISSN = {1868-8969}, year = {2018}, volume = {121}, editor = {Schmid, Ulrich and Widder, Josef}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.DISC.2018.50}, URN = {urn:nbn:de:0030-drops-98392}, doi = {10.4230/LIPIcs.DISC.2018.50}, annote = {Keywords: concurrent specification, concurrent object, linearizability} }
Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)
Simon Forest and Samuel Mimram. Coherence of Gray Categories via Rewriting. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
@InProceedings{forest_et_al:LIPIcs.FSCD.2018.15, author = {Forest, Simon and Mimram, Samuel}, title = {{Coherence of Gray Categories via Rewriting}}, booktitle = {3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}, pages = {15:1--15:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-077-4}, ISSN = {1868-8969}, year = {2018}, volume = {108}, editor = {Kirchner, H\'{e}l\`{e}ne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.15}, URN = {urn:nbn:de:0030-drops-91855}, doi = {10.4230/LIPIcs.FSCD.2018.15}, annote = {Keywords: rewriting, coherence, Gray category, polygraph, pseudomonoid, precategory} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Philippe Malbos and Samuel Mimram. Homological Computations for Term Rewriting Systems. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{malbos_et_al:LIPIcs.FSCD.2016.27, author = {Malbos, Philippe and Mimram, Samuel}, title = {{Homological Computations for Term Rewriting Systems}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {27:1--27:17}, 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.27}, URN = {urn:nbn:de:0030-drops-59821}, doi = {10.4230/LIPIcs.FSCD.2016.27}, annote = {Keywords: term rewriting system, Lawvere theory, Tietze equivalence, resolution, homology, convergent pres entation, coherent presentation} }
Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)
Florence Clerc and Samuel Mimram. Presenting a Category Modulo a Rewriting System. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 89-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{clerc_et_al:LIPIcs.RTA.2015.89, author = {Clerc, Florence and Mimram, Samuel}, title = {{Presenting a Category Modulo a Rewriting System}}, booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)}, pages = {89--105}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-85-9}, ISSN = {1868-8969}, year = {2015}, volume = {36}, editor = {Fern\'{a}ndez, Maribel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.89}, URN = {urn:nbn:de:0030-drops-51916}, doi = {10.4230/LIPIcs.RTA.2015.89}, annote = {Keywords: presentation of a category, quotient category, localization, residuation} }
Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Yves Guiraud, Philippe Malbos, and Samuel Mimram. A Homotopical Completion Procedure with Applications to Coherence of Monoids. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 223-238, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
@InProceedings{guiraud_et_al:LIPIcs.RTA.2013.223, author = {Guiraud, Yves and Malbos, Philippe and Mimram, Samuel}, title = {{A Homotopical Completion Procedure with Applications to Coherence of Monoids}}, booktitle = {24th International Conference on Rewriting Techniques and Applications (RTA 2013)}, pages = {223--238}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-53-8}, ISSN = {1868-8969}, year = {2013}, volume = {21}, editor = {van Raamsdonk, Femke}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.223}, URN = {urn:nbn:de:0030-drops-40649}, doi = {10.4230/LIPIcs.RTA.2013.223}, annote = {Keywords: higher-dimensional rewriting, presentation of monoid, Knuth-Bendix completion, Tietze transformation, low-dimensional homotopy for monoids, coherence} }
Feedback for Dagstuhl Publishing