Published in: LIPIcs, Volume 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Jared Yeager, J. Eliot B. Moss, Michael Norrish, and Philip S. Thomas. Mechanizing Soundness of Off-Policy Evaluation. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 32:1-32:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
@InProceedings{yeager_et_al:LIPIcs.ITP.2022.32, author = {Yeager, Jared and Moss, J. Eliot B. and Norrish, Michael and Thomas, Philip S.}, title = {{Mechanizing Soundness of Off-Policy Evaluation}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {32:1--32:20}, 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.32}, URN = {urn:nbn:de:0030-drops-167413}, doi = {10.4230/LIPIcs.ITP.2022.32}, annote = {Keywords: Formal Methods, HOL4, Reinforcement Learning, Off-Policy Evaluation, Concentration Inequality, Hoeffding} }
Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)
Sam Van den Vonder, Thierry Renaux, Bjarno Oeyen, Joeri De Koster, and Wolfgang De Meuter. Tackling the Awkward Squad for Reactive Programming: The Actor-Reactor Model. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 19:1-19:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{vandenvonder_et_al:LIPIcs.ECOOP.2020.19, author = {Van den Vonder, Sam and Renaux, Thierry and Oeyen, Bjarno and De Koster, Joeri and De Meuter, Wolfgang}, title = {{Tackling the Awkward Squad for Reactive Programming: The Actor-Reactor Model}}, booktitle = {34th European Conference on Object-Oriented Programming (ECOOP 2020)}, pages = {19:1--19:29}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-154-2}, ISSN = {1868-8969}, year = {2020}, volume = {166}, editor = {Hirschfeld, Robert and Pape, Tobias}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.19}, URN = {urn:nbn:de:0030-drops-131768}, doi = {10.4230/LIPIcs.ECOOP.2020.19}, annote = {Keywords: functional reactive programming, reactive programming, reactive streams, actors, reactors} }
Published in: LIPIcs, Volume 162, 17th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2020)
Steven Chaplick, Henry Förster, Myroslav Kryven, and Alexander Wolff. Drawing Graphs with Circular Arcs and Right-Angle Crossings. In 17th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 162, pp. 21:1-21:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
@InProceedings{chaplick_et_al:LIPIcs.SWAT.2020.21, author = {Chaplick, Steven and F\"{o}rster, Henry and Kryven, Myroslav and Wolff, Alexander}, title = {{Drawing Graphs with Circular Arcs and Right-Angle Crossings}}, booktitle = {17th Scandinavian Symposium and Workshops on Algorithm Theory (SWAT 2020)}, pages = {21:1--21:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-150-4}, ISSN = {1868-8969}, year = {2020}, volume = {162}, editor = {Albers, Susanne}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SWAT.2020.21}, URN = {urn:nbn:de:0030-drops-122687}, doi = {10.4230/LIPIcs.SWAT.2020.21}, annote = {Keywords: circular arcs, right-angle crossings, edge density, charging argument} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Peter Lammich. Generating Verified LLVM from Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{lammich:LIPIcs.ITP.2019.22, author = {Lammich, Peter}, title = {{Generating Verified LLVM from Isabelle/HOL}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {22:1--22: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.22}, URN = {urn:nbn:de:0030-drops-110777}, doi = {10.4230/LIPIcs.ITP.2019.22}, annote = {Keywords: Isabelle/HOL, LLVM, Separation Logic, Verification Condition Generator, Code Generation} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Johannes Åman Pohjola, Henrik Rostedt, and Magnus O. Myreen. Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{amanpohjola_et_al:LIPIcs.ITP.2019.32, author = {\r{A}man Pohjola, Johannes and Rostedt, Henrik and Myreen, Magnus O.}, title = {{Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {32:1--32: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.32}, URN = {urn:nbn:de:0030-drops-110872}, doi = {10.4230/LIPIcs.ITP.2019.32}, annote = {Keywords: Program verification, non-termination, liveness, Hoare logic} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Akihisa Yamada and Jérémy Dubut. Complete Non-Orders and Fixed Points. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{yamada_et_al:LIPIcs.ITP.2019.30, author = {Yamada, Akihisa and Dubut, J\'{e}r\'{e}my}, title = {{Complete Non-Orders and Fixed Points}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {30:1--30:16}, 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.30}, URN = {urn:nbn:de:0030-drops-110852}, doi = {10.4230/LIPIcs.ITP.2019.30}, annote = {Keywords: Order Theory, Lattice Theory, Fixed-Points, Isabelle/HOL} }
Published in: LIPIcs, Volume 143, 19th International Workshop on Algorithms in Bioinformatics (WABI 2019)
Natalie Sauerwald, Yihang Shen, and Carl Kingsford. Topological Data Analysis Reveals Principles of Chromosome Structure in Cellular Differentiation. In 19th International Workshop on Algorithms in Bioinformatics (WABI 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 143, pp. 23:1-23:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{sauerwald_et_al:LIPIcs.WABI.2019.23, author = {Sauerwald, Natalie and Shen, Yihang and Kingsford, Carl}, title = {{Topological Data Analysis Reveals Principles of Chromosome Structure in Cellular Differentiation}}, booktitle = {19th International Workshop on Algorithms in Bioinformatics (WABI 2019)}, pages = {23:1--23:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-123-8}, ISSN = {1868-8969}, year = {2019}, volume = {143}, editor = {Huber, Katharina T. and Gusfield, Dan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WABI.2019.23}, URN = {urn:nbn:de:0030-drops-110537}, doi = {10.4230/LIPIcs.WABI.2019.23}, annote = {Keywords: topological data analysis, chromosome structure, Hi-C, topologically associating domains} }
Published in: LIPIcs, Volume 143, 19th International Workshop on Algorithms in Bioinformatics (WABI 2019)
Evgeny Polevikov and Mikhail Kolmogorov. Synteny Paths for Assembly Graphs Comparison. In 19th International Workshop on Algorithms in Bioinformatics (WABI 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 143, pp. 24:1-24:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{polevikov_et_al:LIPIcs.WABI.2019.24, author = {Polevikov, Evgeny and Kolmogorov, Mikhail}, title = {{Synteny Paths for Assembly Graphs Comparison}}, booktitle = {19th International Workshop on Algorithms in Bioinformatics (WABI 2019)}, pages = {24:1--24:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-123-8}, ISSN = {1868-8969}, year = {2019}, volume = {143}, editor = {Huber, Katharina T. and Gusfield, Dan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.WABI.2019.24}, URN = {urn:nbn:de:0030-drops-110545}, doi = {10.4230/LIPIcs.WABI.2019.24}, annote = {Keywords: Assembly graphs, Genome assembly, Synteny blocks, Comparative Genomics} }
Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)
Carl Einarson and Felix Reidl. Domination Above r-Independence: Does Sparseness Help?. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 40:1-40:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{einarson_et_al:LIPIcs.MFCS.2019.40, author = {Einarson, Carl and Reidl, Felix}, title = {{Domination Above r-Independence: Does Sparseness Help?}}, booktitle = {44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)}, pages = {40:1--40:13}, 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.40}, URN = {urn:nbn:de:0030-drops-109840}, doi = {10.4230/LIPIcs.MFCS.2019.40}, annote = {Keywords: Dominating Set, Above Guarantee, Kernel, Bounded Expansion, Nowhere Dense} }
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 140, 30th International Conference on Concurrency Theory (CONCUR 2019)
Lorenzo Clemente, Piotr Hofman, and Patrick Totzke. Timed Basic Parallel Processes. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{clemente_et_al:LIPIcs.CONCUR.2019.15, author = {Clemente, Lorenzo and Hofman, Piotr and Totzke, Patrick}, title = {{Timed Basic Parallel Processes}}, booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)}, pages = {15:1--15:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-121-4}, ISSN = {1868-8969}, year = {2019}, volume = {140}, editor = {Fokkink, Wan and van Glabbeek, Rob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.15}, URN = {urn:nbn:de:0030-drops-109171}, doi = {10.4230/LIPIcs.CONCUR.2019.15}, annote = {Keywords: Timed Automata, Petri Nets} }
Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)
Michael Greenberg. The Dynamic Practice and Static Theory of Gradual Typing. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 6:1-6:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{greenberg:LIPIcs.SNAPL.2019.6, author = {Greenberg, Michael}, title = {{The Dynamic Practice and Static Theory of Gradual Typing}}, booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)}, pages = {6:1--6:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-113-9}, ISSN = {1868-8969}, year = {2019}, volume = {136}, editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.6}, URN = {urn:nbn:de:0030-drops-105495}, doi = {10.4230/LIPIcs.SNAPL.2019.6}, annote = {Keywords: dynamic typing, gradual typing, static typing, implementation, theory, challenge problems} }
Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)
Sheng Chen and John Peter Campora III. Blame Tracking and Type Error Debugging. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 2:1-2:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{chen_et_al:LIPIcs.SNAPL.2019.2, author = {Chen, Sheng and Campora III, John Peter}, title = {{Blame Tracking and Type Error Debugging}}, booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)}, pages = {2:1--2:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-113-9}, ISSN = {1868-8969}, year = {2019}, volume = {136}, editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.2}, URN = {urn:nbn:de:0030-drops-105451}, doi = {10.4230/LIPIcs.SNAPL.2019.2}, annote = {Keywords: Blame tracking, type error debugging, gradual typing, type inference} }
Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)
Will Crichton. From Theory to Systems: A Grounded Approach to Programming Language Education. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 4:1-4:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{crichton:LIPIcs.SNAPL.2019.4, author = {Crichton, Will}, title = {{From Theory to Systems: A Grounded Approach to Programming Language Education}}, booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)}, pages = {4:1--4:9}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-113-9}, ISSN = {1868-8969}, year = {2019}, volume = {136}, editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.4}, URN = {urn:nbn:de:0030-drops-105472}, doi = {10.4230/LIPIcs.SNAPL.2019.4}, annote = {Keywords: programming languages, programming language education} }
Published in: LIPIcs, Volume 136, 3rd Summit on Advances in Programming Languages (SNAPL 2019)
Shriram Krishnamurthi, Benjamin S. Lerner, and Liam Elberty. The Next 700 Semantics: A Research Challenge. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 9:1-9:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{krishnamurthi_et_al:LIPIcs.SNAPL.2019.9, author = {Krishnamurthi, Shriram and Lerner, Benjamin S. and Elberty, Liam}, title = {{The Next 700 Semantics: A Research Challenge}}, booktitle = {3rd Summit on Advances in Programming Languages (SNAPL 2019)}, pages = {9:1--9:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-113-9}, ISSN = {1868-8969}, year = {2019}, volume = {136}, editor = {Lerner, Benjamin S. and Bod{\'\i}k, Rastislav and Krishnamurthi, Shriram}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2019.9}, URN = {urn:nbn:de:0030-drops-105522}, doi = {10.4230/LIPIcs.SNAPL.2019.9}, annote = {Keywords: Programming languages, desugaring, semantics, testing} }
Feedback for Dagstuhl Publishing