Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Franz Baader and Jürgen Giesl. On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{baader_et_al:LIPIcs.FSCD.2024.16, author = {Baader, Franz and Giesl, J\"{u}rgen}, title = {{On the Complexity of the Small Term Reachability Problem for Terminating Term Rewriting Systems}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {16:1--16: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.16}, URN = {urn:nbn:de:0030-drops-203454}, doi = {10.4230/LIPIcs.FSCD.2024.16}, annote = {Keywords: Rewriting, Termination, Confluence, Creating small terms, Derivational complexity, Description Logics, Proof rewriting} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Thiago Felicissimo and Théo Winterhalter. Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{felicissimo_et_al:LIPIcs.FSCD.2024.21, author = {Felicissimo, Thiago and Winterhalter, Th\'{e}o}, title = {{Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {21:1--21:23}, 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.21}, URN = {urn:nbn:de:0030-drops-203503}, doi = {10.4230/LIPIcs.FSCD.2024.21}, annote = {Keywords: Dedukti, Rewriting, Confluence, Dependent types, Cumulativity, Universes} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
René Thiemann and Akihisa Yamada. A Verified Algorithm for Deciding Pattern Completeness. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 27:1-27:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{thiemann_et_al:LIPIcs.FSCD.2024.27, author = {Thiemann, Ren\'{e} and Yamada, Akihisa}, title = {{A Verified Algorithm for Deciding Pattern Completeness}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {27:1--27:17}, 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.27}, URN = {urn:nbn:de:0030-drops-203566}, doi = {10.4230/LIPIcs.FSCD.2024.27}, annote = {Keywords: Isabelle/HOL, pattern matching, term rewriting} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Takahito Aoto, Naoki Nishida, and Jonas Schöpf. Equational Theories and Validity for Logically Constrained Term Rewriting. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 31:1-31:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{aoto_et_al:LIPIcs.FSCD.2024.31, author = {Aoto, Takahito and Nishida, Naoki and Sch\"{o}pf, Jonas}, title = {{Equational Theories and Validity for Logically Constrained Term Rewriting}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {31:1--31:21}, 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.31}, URN = {urn:nbn:de:0030-drops-203607}, doi = {10.4230/LIPIcs.FSCD.2024.31}, annote = {Keywords: constrained equation, constrained equational theory, logically constrained term rewriting, algebraic semantics, consistency} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Salvador Lucas. Termination of Generalized Term Rewriting Systems. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 32:1-32:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{lucas:LIPIcs.FSCD.2024.32, author = {Lucas, Salvador}, title = {{Termination of Generalized Term Rewriting Systems}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {32:1--32: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.32}, URN = {urn:nbn:de:0030-drops-203616}, doi = {10.4230/LIPIcs.FSCD.2024.32}, annote = {Keywords: Program Analysis, Reduction-Based Systems, Termination} }
Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)
Raphael Douglas Giles, Vincent Jackson, and Christine Rizkallah. T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 139:1-139:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{giles_et_al:LIPIcs.ICALP.2024.139, author = {Giles, Raphael Douglas and Jackson, Vincent and Rizkallah, Christine}, title = {{T-Rex: Termination of Recursive Functions Using Lexicographic Linear Combinations}}, booktitle = {51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)}, pages = {139:1--139:19}, 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.139}, URN = {urn:nbn:de:0030-drops-202827}, doi = {10.4230/LIPIcs.ICALP.2024.139}, annote = {Keywords: Termination, Recursive functions} }
Published in: LIPIcs, Volume 275, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)
Emin Karayel. An Embarrassingly Parallel Optimal-Space Cardinality Estimation Algorithm. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 275, pp. 35:1-35:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{karayel:LIPIcs.APPROX/RANDOM.2023.35, author = {Karayel, Emin}, title = {{An Embarrassingly Parallel Optimal-Space Cardinality Estimation Algorithm}}, booktitle = {Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2023)}, pages = {35:1--35:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-296-9}, ISSN = {1868-8969}, year = {2023}, volume = {275}, editor = {Megow, Nicole and Smith, Adam}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2023.35}, URN = {urn:nbn:de:0030-drops-188607}, doi = {10.4230/LIPIcs.APPROX/RANDOM.2023.35}, annote = {Keywords: Distinct Elements, Distributed Algorithms, Randomized Algorithms, Expander Graphs, Derandomization, Sketching} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Oskar Abrahamsson and Magnus O. Myreen. Fast, Verified Computation for Candle. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 4:1-4:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{abrahamsson_et_al:LIPIcs.ITP.2023.4, author = {Abrahamsson, Oskar and Myreen, Magnus O.}, title = {{Fast, Verified Computation for Candle}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {4:1--4:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.4}, URN = {urn:nbn:de:0030-drops-183797}, doi = {10.4230/LIPIcs.ITP.2023.4}, annote = {Keywords: Prover soundness, Higher-order logic, Interactive theorem proving} }
Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)
Balazs Toth and Tobias Nipkow. Real-Time Double-Ended Queue Verified (Proof Pearl). In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{toth_et_al:LIPIcs.ITP.2023.29, author = {Toth, Balazs and Nipkow, Tobias}, title = {{Real-Time Double-Ended Queue Verified (Proof Pearl)}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {29:1--29:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-284-6}, ISSN = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.29}, URN = {urn:nbn:de:0030-drops-184044}, doi = {10.4230/LIPIcs.ITP.2023.29}, annote = {Keywords: Double-ended queue, data structures, verification, Isabelle} }
Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Emin Karayel. Formalization of Randomized Approximation Algorithms for Frequency Moments. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 21:1-21:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{karayel:LIPIcs.ITP.2022.21, author = {Karayel, Emin}, title = {{Formalization of Randomized Approximation Algorithms for Frequency Moments}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {21:1--21:21}, 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.21}, URN = {urn:nbn:de:0030-drops-167308}, doi = {10.4230/LIPIcs.ITP.2022.21}, annote = {Keywords: Formal Verification, Isabelle/HOL, Randomized Algorithms, Frequency Moments} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Julian Brunner, Benedikt Seidl, and Salomon Sickert. A Verified and Compositional Translation of LTL to Deterministic Rabin Automata. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 11:1-11:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{brunner_et_al:LIPIcs.ITP.2019.11, author = {Brunner, Julian and Seidl, Benedikt and Sickert, Salomon}, title = {{A Verified and Compositional Translation of LTL to Deterministic Rabin Automata}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {11:1--11: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.11}, URN = {urn:nbn:de:0030-drops-110664}, doi = {10.4230/LIPIcs.ITP.2019.11}, annote = {Keywords: Automata Theory, Automata over Infinite Words, Deterministic Automata, Linear Temporal Logic, Model Checking, Verified Algorithms} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Peter Lammich and Tobias Nipkow. Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{lammich_et_al:LIPIcs.ITP.2019.23, author = {Lammich, Peter and Nipkow, Tobias}, title = {{Proof Pearl: Purely Functional, Simple and Efficient Priority Search Trees and Applications to Prim and Dijkstra}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {23:1--23:18}, 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.23}, URN = {urn:nbn:de:0030-drops-110788}, doi = {10.4230/LIPIcs.ITP.2019.23}, annote = {Keywords: Priority queue, Dijkstra’s algorithm, Prim’s algorithm, verification, Isabelle} }
Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)
Mohammad Abdulaziz, Kurt Mehlhorn, and Tobias Nipkow. Trustworthy Graph Algorithms (Invited Talk). In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 1:1-1:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{abdulaziz_et_al:LIPIcs.MFCS.2019.1, author = {Abdulaziz, Mohammad and Mehlhorn, Kurt and Nipkow, Tobias}, title = {{Trustworthy Graph Algorithms}}, booktitle = {44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)}, pages = {1:1--1:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-117-7}, ISSN = {1868-8969}, year = {2019}, volume = {138}, editor = {Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.1}, URN = {urn:nbn:de:0030-drops-109456}, doi = {10.4230/LIPIcs.MFCS.2019.1}, annote = {Keywords: graph algorithms, formal correct proofs, Isabelle, LEDA, certifying algorithms} }
Published in: LIPIcs, Volume 104, 23rd International Conference on Types for Proofs and Programs (TYPES 2017)
Julius Michaelis and Tobias Nipkow. Formalized Proof Systems for Propositional Logic. In 23rd International Conference on Types for Proofs and Programs (TYPES 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 104, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{michaelis_et_al:LIPIcs.TYPES.2017.5, author = {Michaelis, Julius and Nipkow, Tobias}, title = {{Formalized Proof Systems for Propositional Logic}}, booktitle = {23rd International Conference on Types for Proofs and Programs (TYPES 2017)}, pages = {5:1--5:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-071-2}, ISSN = {1868-8969}, year = {2019}, volume = {104}, editor = {Abel, Andreas and Nordvall Forsberg, Fredrik and Kaposi, Ambrus}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2017.5}, URN = {urn:nbn:de:0030-drops-100537}, doi = {10.4230/LIPIcs.TYPES.2017.5}, annote = {Keywords: formalization of logic, proof systems, sequent calculus, natural deduction, resolution} }
Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)
Maximilian P. L. Haslbeck and Tobias Nipkow. Verified Analysis of List Update Algorithms. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 49:1-49:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
@InProceedings{haslbeck_et_al:LIPIcs.FSTTCS.2016.49, author = {Haslbeck, Maximilian P. L. and Nipkow, Tobias}, title = {{Verified Analysis of List Update Algorithms}}, booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)}, pages = {49:1--49:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-027-9}, ISSN = {1868-8969}, year = {2016}, volume = {65}, editor = {Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.49}, URN = {urn:nbn:de:0030-drops-68849}, doi = {10.4230/LIPIcs.FSTTCS.2016.49}, annote = {Keywords: Program Verification, Algorithm Analysis, Online Algorithms} }