Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Martin Desharnais, Petar Vukmirović, Jasmin Blanchette, and Makarius Wenzel. Seventeen Provers Under the Hammer. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 8:1-8:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{desharnais_et_al:LIPIcs.ITP.2022.8, author = {Desharnais, Martin and Vukmirovi\'{c}, Petar and Blanchette, Jasmin and Wenzel, Makarius}, title = {{Seventeen Provers Under the Hammer}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {8:1--8:18}, 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.8}, URN = {urn:nbn:de:0030-drops-167178}, doi = {10.4230/LIPIcs.ITP.2022.8}, annote = {Keywords: Automatic theorem proving, interactive theorem proving, proof assistants} }
Published in: LIPIcs, Volume 220, 25th International Conference on Database Theory (ICDT 2022)
Martin Raszyk, David Basin, Srđan Krstić, and Dmitriy Traytel. Practical Relational Calculus Query Evaluation. In 25th International Conference on Database Theory (ICDT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 220, pp. 11:1-11:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{raszyk_et_al:LIPIcs.ICDT.2022.11, author = {Raszyk, Martin and Basin, David and Krsti\'{c}, Sr{\d}an and Traytel, Dmitriy}, title = {{Practical Relational Calculus Query Evaluation}}, booktitle = {25th International Conference on Database Theory (ICDT 2022)}, pages = {11:1--11:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-223-5}, ISSN = {1868-8969}, year = {2022}, volume = {220}, editor = {Olteanu, Dan and Vortmeier, Nils}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2022.11}, URN = {urn:nbn:de:0030-drops-158857}, doi = {10.4230/LIPIcs.ICDT.2022.11}, annote = {Keywords: Relational calculus, relative safety, safe-range, query translation} }
Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)
Matthias Brun, Sára Decova, Andrea Lattuada, and Dmitriy Traytel. Verified Progress Tracking for Timely Dataflow. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 10:1-10:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)
@InProceedings{brun_et_al:LIPIcs.ITP.2021.10, author = {Brun, Matthias and Decova, S\'{a}ra and Lattuada, Andrea and Traytel, Dmitriy}, title = {{Verified Progress Tracking for Timely Dataflow}}, booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)}, pages = {10:1--10: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.10}, URN = {urn:nbn:de:0030-drops-139057}, doi = {10.4230/LIPIcs.ITP.2021.10}, annote = {Keywords: safety, distributed systems, timely dataflow, Isabelle/HOL} }
Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)
Petar Vukmirović, Alexander Bentkamp, and Visa Nummelin. Efficient Full Higher-Order Unification. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 5:1-5:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
@InProceedings{vukmirovic_et_al:LIPIcs.FSCD.2020.5, author = {Vukmirovi\'{c}, Petar and Bentkamp, Alexander and Nummelin, Visa}, title = {{Efficient Full Higher-Order Unification}}, booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}, pages = {5:1--5:17}, 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.5}, URN = {urn:nbn:de:0030-drops-123271}, doi = {10.4230/LIPIcs.FSCD.2020.5}, annote = {Keywords: unification, higher-order logic, theorem proving, term rewriting, indexing data structures} }
Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)
Henning Basold. Coinduction in Flow: The Later Modality in Fibrations. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{basold:LIPIcs.CALCO.2019.8, author = {Basold, Henning}, title = {{Coinduction in Flow: The Later Modality in Fibrations}}, booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)}, pages = {8:1--8:22}, 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.8}, URN = {urn:nbn:de:0030-drops-114369}, doi = {10.4230/LIPIcs.CALCO.2019.8}, annote = {Keywords: Coinduction, Fibrations, Later Modality, Recursive Proofs, Up-to techniques, Probabilistic Logic, Probabilistic Programming} }
Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)
Damien Pous. Coinduction: Automata, Formal Proof, Companions (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 4:1-4:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{pous:LIPIcs.CALCO.2019.4, author = {Pous, Damien}, title = {{Coinduction: Automata, Formal Proof, Companions}}, booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)}, pages = {4:1--4:4}, 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.4}, URN = {urn:nbn:de:0030-drops-114323}, doi = {10.4230/LIPIcs.CALCO.2019.4}, annote = {Keywords: Coinduction, Automata, Coalgebra, Formal proofs} }
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)
Jeremy Avigad, Mario Carneiro, and Simon Hudon. Data Types as Quotients of Polynomial Functors. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{avigad_et_al:LIPIcs.ITP.2019.6, author = {Avigad, Jeremy and Carneiro, Mario and Hudon, Simon}, title = {{Data Types as Quotients of Polynomial Functors}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {6:1--6: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.6}, URN = {urn:nbn:de:0030-drops-110612}, doi = {10.4230/LIPIcs.ITP.2019.6}, annote = {Keywords: data types, polynomial functors, inductive types, coinductive types} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Enrico Tassi. Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{tassi:LIPIcs.ITP.2019.29, author = {Tassi, Enrico}, title = {{Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {29:1--29: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.29}, URN = {urn:nbn:de:0030-drops-110841}, doi = {10.4230/LIPIcs.ITP.2019.29}, annote = {Keywords: Coq, Containers, Induction, Equality test, Parametricity translation} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Matthias Brun and Dmitriy Traytel. Generic Authenticated Data Structures, Formally. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{brun_et_al:LIPIcs.ITP.2019.10, author = {Brun, Matthias and Traytel, Dmitriy}, title = {{Generic Authenticated Data Structures, Formally}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {10:1--10: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.10}, URN = {urn:nbn:de:0030-drops-110657}, doi = {10.4230/LIPIcs.ITP.2019.10}, annote = {Keywords: Authenticated Data Structures, Verifiable Computation, Isabelle/HOL, Nominal Isabelle} }
Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)
Martin Raszyk, David Basin, and Dmitriy Traytel. From Nondeterministic to Multi-Head Deterministic Finite-State Transducers (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 127:1-127:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
@InProceedings{raszyk_et_al:LIPIcs.ICALP.2019.127, author = {Raszyk, Martin and Basin, David and Traytel, Dmitriy}, title = {{From Nondeterministic to Multi-Head Deterministic Finite-State Transducers}}, booktitle = {46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)}, pages = {127:1--127:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-109-2}, ISSN = {1868-8969}, year = {2019}, volume = {132}, editor = {Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.127}, URN = {urn:nbn:de:0030-drops-107037}, doi = {10.4230/LIPIcs.ICALP.2019.127}, annote = {Keywords: Formal languages, Nondeterminism, Multi-head automata, Finite transducers} }
Published in: LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Jasmin Christian Blanchette, Mathias Fleury, and Dmitriy Traytel. Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 11:1-11:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
@InProceedings{blanchette_et_al:LIPIcs.FSCD.2017.11, author = {Blanchette, Jasmin Christian and Fleury, Mathias and Traytel, Dmitriy}, title = {{Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in Isabelle/HOL}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {11:1--11:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.11}, URN = {urn:nbn:de:0030-drops-77155}, doi = {10.4230/LIPIcs.FSCD.2017.11}, annote = {Keywords: Multisets, ordinals, proof assistants} }
Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Dmitriy Traytel. Formal Languages, Formally and Coinductively. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 31:1-31:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)
@InProceedings{traytel:LIPIcs.FSCD.2016.31, author = {Traytel, Dmitriy}, title = {{Formal Languages, Formally and Coinductively}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {31:1--31: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.31}, URN = {urn:nbn:de:0030-drops-59853}, doi = {10.4230/LIPIcs.FSCD.2016.31}, annote = {Keywords: Formal languages, codatatypes, corecursion, coinduction, interactive theorem proving, Isabelle HOL} }
Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)
Dmitriy Traytel. A Coalgebraic Decision Procedure for WS1S. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 487-503, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{traytel:LIPIcs.CSL.2015.487, author = {Traytel, Dmitriy}, title = {{A Coalgebraic Decision Procedure for WS1S}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {487--503}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.487}, URN = {urn:nbn:de:0030-drops-54335}, doi = {10.4230/LIPIcs.CSL.2015.487}, annote = {Keywords: WS1S, decision procedure, coalgebra, Brzozowski derivatives, Isabelle} }
Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)
Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, and Tjark Weber. Modal Logics for Nominal Transition Systems. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 198-211, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
@InProceedings{parrow_et_al:LIPIcs.CONCUR.2015.198, author = {Parrow, Joachim and Borgstr\"{o}m, Johannes and Eriksson, Lars-Henrik and Gutkovas, Ramunas and Weber, Tjark}, title = {{Modal Logics for Nominal Transition Systems}}, booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)}, pages = {198--211}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-91-0}, ISSN = {1868-8969}, year = {2015}, volume = {42}, editor = {Aceto, Luca and de Frutos Escrig, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.198}, URN = {urn:nbn:de:0030-drops-53823}, doi = {10.4230/LIPIcs.CONCUR.2015.198}, annote = {Keywords: Process algebra, nominal sets, bisimulation, modal logic} }
Feedback for Dagstuhl Publishing