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} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Tobias Nipkow. Verified Analysis of Functional Data Structures. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 4:1-4:2, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)
@InProceedings{nipkow:LIPIcs.FSCD.2016.4, author = {Nipkow, Tobias}, title = {{Verified Analysis of Functional Data Structures}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {4:1--4:2}, 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.4}, URN = {urn:nbn:de:0030-drops-59701}, doi = {10.4230/LIPIcs.FSCD.2016.4}, annote = {Keywords: Program Verification, Algorithm Analysis, Functional Programming} }
Published in: Dagstuhl Reports, Volume 3, Issue 10 (2014)
Nikolaj Bjorner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach. Deduction and Arithmetic (Dagstuhl Seminar 13411). In Dagstuhl Reports, Volume 3, Issue 10, pp. 1-24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2014)
@Article{bjorner_et_al:DagRep.3.10.1, author = {Bjorner, Nikolaj and H\"{a}hnle, Reiner and Nipkow, Tobias and Weidenbach, Christoph}, title = {{Deduction and Arithmetic (Dagstuhl Seminar 13411)}}, pages = {1--24}, journal = {Dagstuhl Reports}, ISSN = {2192-5283}, year = {2014}, volume = {3}, number = {10}, editor = {Bjorner, Nikolaj and H\"{a}hnle, Reiner and Nipkow, Tobias and Weidenbach, Christoph}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.10.1}, URN = {urn:nbn:de:0030-drops-44250}, doi = {10.4230/DagRep.3.10.1}, annote = {Keywords: Automated Deduction; Program Verification; Arithmetic Constraint Solving} }
Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)
Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow. 09411 Abstracts Collection – Interaction versus Automation: The two Faces of Deduction. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)
@InProceedings{ball_et_al:DagSemProc.09411.1, author = {Ball, Thomas and Giesl, J\"{u}rgen and H\"{a}hnle, Reiner and Nipkow, Tobias}, title = {{09411 Abstracts Collection – Interaction versus Automation: The two Faces of Deduction}}, booktitle = {Interaction versus Automation: The two Faces of Deduction}, pages = {1--18}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {9411}, editor = {Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.1}, URN = {urn:nbn:de:0030-drops-25032}, doi = {10.4230/DagSemProc.09411.1}, annote = {Keywords: Formal Logic, Deduction, Artificial Intelligence} }
Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)
Thomas Ball, Jürgen Giesl, Reiner Hähnle, and Tobias Nipkow. 09411 Executive Summary – Interaction versus Automation: The two Faces of Deductions. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)
@InProceedings{ball_et_al:DagSemProc.09411.2, author = {Ball, Thomas and Giesl, J\"{u}rgen and H\"{a}hnle, Reiner and Nipkow, Tobias}, title = {{09411 Executive Summary – Interaction versus Automation: The two Faces of Deductions}}, booktitle = {Interaction versus Automation: The two Faces of Deduction}, pages = {1--4}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {9411}, editor = {Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.2}, URN = {urn:nbn:de:0030-drops-24213}, doi = {10.4230/DagSemProc.09411.2}, annote = {Keywords: Formal Logic, Deduction, Artificial Intelligence} }
Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)
Viorica Sofronie-Stokkermans. Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-33, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)
@InProceedings{sofroniestokkermans:DagSemProc.09411.3, author = {Sofronie-Stokkermans, Viorica}, title = {{Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms}}, booktitle = {Interaction versus Automation: The two Faces of Deduction}, pages = {1--33}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {9411}, editor = {Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.3}, URN = {urn:nbn:de:0030-drops-24241}, doi = {10.4230/DagSemProc.09411.3}, annote = {Keywords: Decision procedures, recursive datatypes, recursive functions, homomorphisms, verification, cryptography} }
Published in: Dagstuhl Seminar Proceedings, Volume 9411, Interaction versus Automation: The two Faces of Deduction (2010)
Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, and Peter Schneider-Kamp. Inductive Theorem Proving meets Dependency Pairs. In Interaction versus Automation: The two Faces of Deduction. Dagstuhl Seminar Proceedings, Volume 9411, pp. 1-4, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2010)
@InProceedings{swiderski_et_al:DagSemProc.09411.4, author = {Swiderski, Stephan and Parting, Michael and Giesl, J\"{u}rgen and Fuhs, Carsten and Schneider-Kamp, Peter}, title = {{Inductive Theorem Proving meets Dependency Pairs}}, booktitle = {Interaction versus Automation: The two Faces of Deduction}, pages = {1--4}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {9411}, editor = {Thomas Ball and J\"{u}rgen Giesl and Reiner H\"{a}hnle and Tobias Nipkow}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09411.4}, URN = {urn:nbn:de:0030-drops-24220}, doi = {10.4230/DagSemProc.09411.4}, annote = {Keywords: Termination, Term Rewriting, Dependency Pairs, Inductive Theorem Proving} }
Feedback for Dagstuhl Publishing