Published in: LIPIcs, Volume 308, 32nd Annual European Symposium on Algorithms (ESA 2024)
Elfarouk Harb, Zhengcheng Huang, and Da Wei Zheng. Shortest Path Separators in Unit Disk Graphs. In 32nd Annual European Symposium on Algorithms (ESA 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 308, pp. 66:1-66:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{harb_et_al:LIPIcs.ESA.2024.66, author = {Harb, Elfarouk and Huang, Zhengcheng and Zheng, Da Wei}, title = {{Shortest Path Separators in Unit Disk Graphs}}, booktitle = {32nd Annual European Symposium on Algorithms (ESA 2024)}, pages = {66:1--66:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-338-6}, ISSN = {1868-8969}, year = {2024}, volume = {308}, editor = {Chan, Timothy and Fischer, Johannes and Iacono, John and Herman, Grzegorz}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2024.66}, URN = {urn:nbn:de:0030-drops-211375}, doi = {10.4230/LIPIcs.ESA.2024.66}, annote = {Keywords: Balanced shortest path separators, unit disk graphs, crossings} }
Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)
Ashton Wiersdorf, Stephen Chang, Matthias Felleisen, and Ben Greenman. Type Tailoring. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 44:1-44:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{wiersdorf_et_al:LIPIcs.ECOOP.2024.44, author = {Wiersdorf, Ashton and Chang, Stephen and Felleisen, Matthias and Greenman, Ben}, title = {{Type Tailoring}}, booktitle = {38th European Conference on Object-Oriented Programming (ECOOP 2024)}, pages = {44:1--44:27}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-341-6}, ISSN = {1868-8969}, year = {2024}, volume = {313}, editor = {Aldrich, Jonathan and Salvaneschi, Guido}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.44}, URN = {urn:nbn:de:0030-drops-208933}, doi = {10.4230/LIPIcs.ECOOP.2024.44}, annote = {Keywords: Types, Metaprogramming, Macros, Partial Evaluation} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Ślusarz, and Kathrin Stark. Taming Differentiable Logics with Coq Formalisation. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{affeldt_et_al:LIPIcs.ITP.2024.4, author = {Affeldt, Reynald and Bruni, Alessandro and Komendantskaya, Ekaterina and \'{S}lusarz, Natalia and Stark, Kathrin}, title = {{Taming Differentiable Logics with Coq Formalisation}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {4:1--4:19}, 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.4}, URN = {urn:nbn:de:0030-drops-207325}, doi = {10.4230/LIPIcs.ITP.2024.4}, annote = {Keywords: Machine Learning, Loss Functions, Differentiable Logics, Logic and Semantics, Interactive Theorem Proving} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Reynald Affeldt and Zachary Stone. A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{affeldt_et_al:LIPIcs.ITP.2024.5, author = {Affeldt, Reynald and Stone, Zachary}, title = {{A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {5:1--5:19}, 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.5}, URN = {urn:nbn:de:0030-drops-207330}, doi = {10.4230/LIPIcs.ITP.2024.5}, annote = {Keywords: Coq proof assistant, Mathematical Components library, Lebesgue integral, fundamental theorem of calculus} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Dagur Asgeirsson. Towards Solid Abelian Groups: A Formal Proof of Nöbeling’s Theorem. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 6:1-6:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{asgeirsson:LIPIcs.ITP.2024.6, author = {Asgeirsson, Dagur}, title = {{Towards Solid Abelian Groups: A Formal Proof of N\"{o}beling’s Theorem}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {6:1--6:17}, 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.6}, URN = {urn:nbn:de:0030-drops-207347}, doi = {10.4230/LIPIcs.ITP.2024.6}, annote = {Keywords: Condensed mathematics, N\"{o}beling’s theorem, Lean, Mathlib, Interactive theorem proving} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, and Mauricio Ayala-Rincón. A Formalization of the General Theory of Quaternions. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 11:1-11:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{delima_et_al:LIPIcs.ITP.2024.11, author = {de Lima, Thaynara Arielly and Galdino, Andr\'{e} Luiz and de Oliveira Ribeiro, Bruno Berto and Ayala-Rinc\'{o}n, Mauricio}, title = {{A Formalization of the General Theory of Quaternions}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {11:1--11: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.11}, URN = {urn:nbn:de:0030-drops-207398}, doi = {10.4230/LIPIcs.ITP.2024.11}, annote = {Keywords: Theory of quaternions, Hamilton’s quaternions, Algebraic formalizations, PVS} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Jacques Garrigue and Takafumi Saikawa. Typed Compositional Quantum Computation with Lenses. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 15:1-15:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{garrigue_et_al:LIPIcs.ITP.2024.15, author = {Garrigue, Jacques and Saikawa, Takafumi}, title = {{Typed Compositional Quantum Computation with Lenses}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {15:1--15: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.15}, URN = {urn:nbn:de:0030-drops-207431}, doi = {10.4230/LIPIcs.ITP.2024.15}, annote = {Keywords: quantum programming, semantics, lens, currying, Coq, MathComp} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Yann Leray, Gaëtan Gilbert, Nicolas Tabareau, and Théo Winterhalter. The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 26:1-26:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{leray_et_al:LIPIcs.ITP.2024.26, author = {Leray, Yann and Gilbert, Ga\"{e}tan and Tabareau, Nicolas and Winterhalter, Th\'{e}o}, title = {{The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {26:1--26: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.26}, URN = {urn:nbn:de:0030-drops-207545}, doi = {10.4230/LIPIcs.ITP.2024.26}, annote = {Keywords: type theory, dependent types, rewrite rules, type preservation, Coq} }
Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)
Sewon Park and Holger Thies. A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{park_et_al:LIPIcs.ITP.2024.30, author = {Park, Sewon and Thies, Holger}, title = {{A Coq Formalization of Taylor Models and Power Series for Solving Ordinary Differential Equations}}, booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)}, pages = {30:1--30:19}, 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.30}, URN = {urn:nbn:de:0030-drops-207581}, doi = {10.4230/LIPIcs.ITP.2024.30}, annote = {Keywords: Exact real computation, Taylor models, Analytic functions, Computable analysis, Program extraction} }
Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)
Dmitry Chistikov, Jérôme Leroux, Henry Sinclair-Banks, and Nicolas Waldburger. Invariants for One-Counter Automata with Disequality Tests. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 17:1-17:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{chistikov_et_al:LIPIcs.CONCUR.2024.17, author = {Chistikov, Dmitry and Leroux, J\'{e}r\^{o}me and Sinclair-Banks, Henry and Waldburger, Nicolas}, title = {{Invariants for One-Counter Automata with Disequality Tests}}, booktitle = {35th International Conference on Concurrency Theory (CONCUR 2024)}, pages = {17:1--17:21}, 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.17}, URN = {urn:nbn:de:0030-drops-207898}, doi = {10.4230/LIPIcs.CONCUR.2024.17}, annote = {Keywords: Inductive invariant, Vector addition system, One-counter automaton} }
Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)
Joris Ceulemans, Andreas Nuyts, and Dominique Devriese. A Sound and Complete Substitution Algorithm for Multimode Type Theory. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 4:1-4:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{ceulemans_et_al:LIPIcs.TYPES.2023.4, author = {Ceulemans, Joris and Nuyts, Andreas and Devriese, Dominique}, title = {{A Sound and Complete Substitution Algorithm for Multimode Type Theory}}, booktitle = {29th International Conference on Types for Proofs and Programs (TYPES 2023)}, pages = {4:1--4:23}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-332-4}, ISSN = {1868-8969}, year = {2024}, volume = {303}, editor = {Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.4}, URN = {urn:nbn:de:0030-drops-204826}, doi = {10.4230/LIPIcs.TYPES.2023.4}, annote = {Keywords: dependent type theory, modalities, multimode type theory, explicit substitutions, substitution algorithm} }
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 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
Tsvi Kopelowitz, Ariel Korin, and Liam Roditty. On the Space Usage of Approximate Distance Oracles with Sub-2 Stretch. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 101:1-101:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{kopelowitz_et_al:LIPIcs.ICALP.2024.101, author = {Kopelowitz, Tsvi and Korin, Ariel and Roditty, Liam}, title = {{On the Space Usage of Approximate Distance Oracles with Sub-2 Stretch}}, booktitle = {51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)}, pages = {101:1--101:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-322-5}, ISSN = {1868-8969}, year = {2024}, volume = {297}, editor = {Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.101}, URN = {urn:nbn:de:0030-drops-202443}, doi = {10.4230/LIPIcs.ICALP.2024.101}, annote = {Keywords: Graph algorithms, Approximate distance oracle, data structures, shortest path} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Sophie Bernard, Cyril Cohen, Assia Mahboubi, and Pierre-Yves Strub. Unsolvability of the Quintic Formalized in Dependent Type Theory. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{bernard_et_al:LIPIcs.ITP.2021.8, author = {Bernard, Sophie and Cohen, Cyril and Mahboubi, Assia and Strub, Pierre-Yves}, title = {{Unsolvability of the Quintic Formalized in Dependent Type Theory}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {8:1--8:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-188-7}, ISSN = {1868-8969}, year = {2021}, volume = {193}, editor = {Cohen, Liron and Kaliszyk, Cezary}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.8}, URN = {urn:nbn:de:0030-drops-139038}, doi = {10.4230/LIPIcs.ITP.2021.8}, annote = {Keywords: Galois theory, Coq, Mathematical Components, Dependent Type Theory, Abel-Ruffini, General quintic} }
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 34:1-34:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{cohen_et_al:LIPIcs.FSCD.2020.34, author = {Cohen, Cyril and Sakaguchi, Kazuhiko and Tassi, Enrico}, title = {{Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {34:1--34:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-155-9}, ISSN = {1868-8969}, year = {2020}, volume = {167}, editor = {Ariola, Zena M.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.34}, URN = {urn:nbn:de:0030-drops-123562}, doi = {10.4230/LIPIcs.FSCD.2020.34}, annote = {Keywords: Algebraic Hierarchy, Packed Classes, Coq, Elpi, Metaprogramming, \lambdaProlog} }
Feedback for Dagstuhl Publishing