Published in: LIPIcs, Volume 308, 32nd Annual European Symposium on Algorithms (ESA 2024)
Alexander Naumann, Annika Bonerath, and Jan-Henrik Haunert. Many-To-Many Polygon Matching à La Jaccard. In 32nd Annual European Symposium on Algorithms (ESA 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 308, pp. 90:1-90:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{naumann_et_al:LIPIcs.ESA.2024.90, author = {Naumann, Alexander and Bonerath, Annika and Haunert, Jan-Henrik}, title = {{Many-To-Many Polygon Matching \`{a} La Jaccard}}, booktitle = {32nd Annual European Symposium on Algorithms (ESA 2024)}, pages = {90:1--90:15}, 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.90}, URN = {urn:nbn:de:0030-drops-211614}, doi = {10.4230/LIPIcs.ESA.2024.90}, annote = {Keywords: polygon matching, exact algorithm, Jaccard index} }
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 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Yannick Forster, Fabian Kunze, and Nils Lauermann. Synthetic Kolmogorov Complexity in Coq. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 12:1-12:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{forster_et_al:LIPIcs.ITP.2022.12, author = {Forster, Yannick and Kunze, Fabian and Lauermann, Nils}, title = {{Synthetic Kolmogorov Complexity in Coq}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {12:1--12:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-252-5}, ISSN = {1868-8969}, year = {2022}, volume = {237}, editor = {Andronick, June and de Moura, Leonardo}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2022.12}, URN = {urn:nbn:de:0030-drops-167219}, doi = {10.4230/LIPIcs.ITP.2022.12}, annote = {Keywords: Kolmogorov complexity, computability theory, random numbers, constructive matemathics, synthetic computability theory, constructive type theory, Coq} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Yannick Forster, Fabian Kunze, Gert Smolka, and Maximilian Wuttke. A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{forster_et_al:LIPIcs.ITP.2021.19, author = {Forster, Yannick and Kunze, Fabian and Smolka, Gert and Wuttke, Maximilian}, title = {{A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value \lambda-Calculus}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {19:1--19:20}, 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.19}, URN = {urn:nbn:de:0030-drops-139142}, doi = {10.4230/LIPIcs.ITP.2021.19}, annote = {Keywords: formalizations of computational models, computability theory, Coq, time complexity, Turing machines, lambda calculus, Hoare logic} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Lennard Gäher and Fabian Kunze. Mechanising Complexity Theory: The Cook-Levin Theorem in Coq. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
@InProceedings{gaher_et_al:LIPIcs.ITP.2021.20, author = {G\"{a}her, Lennard and Kunze, Fabian}, title = {{Mechanising Complexity Theory: The Cook-Levin Theorem in Coq}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {20:1--20: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.20}, URN = {urn:nbn:de:0030-drops-139154}, doi = {10.4230/LIPIcs.ITP.2021.20}, annote = {Keywords: computational model, NP completeness, Coq, Cook, Levin} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Yannick Forster and Fabian Kunze. A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{forster_et_al:LIPIcs.ITP.2019.17, author = {Forster, Yannick and Kunze, Fabian}, title = {{A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {17:1--17:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-122-1}, ISSN = {1868-8969}, year = {2019}, volume = {141}, editor = {Harrison, John and O'Leary, John and Tolmach, Andrew}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.17}, URN = {urn:nbn:de:0030-drops-110724}, doi = {10.4230/LIPIcs.ITP.2019.17}, annote = {Keywords: call-by-value, lambda calculus, Coq, constructive type theory, extraction, computability} }
Feedback for Dagstuhl Publishing