LIPIcs, Volume 141
ITP 2019, September 9-12, 2019, Portland, OR, USA
Editors: John Harrison, John O'Leary, and Andrew Tolmach
Published in: OASIcs, Volume 109, Eelco Visser Commemorative Symposium (EVCS 2023)
Andrew Tolmach. Eelco Visser: The Oregon Connection. In Eelco Visser Commemorative Symposium (EVCS 2023). Open Access Series in Informatics (OASIcs), Volume 109, pp. 27:1-27:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
@InProceedings{tolmach:OASIcs.EVCS.2023.27, author = {Tolmach, Andrew}, title = {{Eelco Visser: The Oregon Connection}}, booktitle = {Eelco Visser Commemorative Symposium (EVCS 2023)}, pages = {27:1--27:6}, series = {Open Access Series in Informatics (OASIcs)}, ISBN = {978-3-95977-267-9}, ISSN = {2190-6807}, year = {2023}, volume = {109}, editor = {L\"{a}mmel, Ralf and Mosses, Peter D. and Steimann, Friedrich}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.EVCS.2023.27}, URN = {urn:nbn:de:0030-drops-177971}, doi = {10.4230/OASIcs.EVCS.2023.27}, annote = {Keywords: Eelco Visser, Stratego, scope graphs} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@Proceedings{harrison_et_al:LIPIcs.ITP.2019, title = {{LIPIcs, Volume 141, ITP'19, Complete Volume}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019}, URN = {urn:nbn:de:0030-drops-112972}, doi = {10.4230/LIPIcs.ITP.2019}, annote = {Keywords: Theory of computation, Logic} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 0:i-0:xiv, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{harrison_et_al:LIPIcs.ITP.2019.0, author = {Harrison, John and O'Leary, John and Tolmach, Andrew}, title = {{Front Matter, Table of Contents, Preface, Conference Organization}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {0:i--0:xiv}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.0}, URN = {urn:nbn:de:0030-drops-110550}, doi = {10.4230/LIPIcs.ITP.2019.0}, annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
June Andronick. A Million Lines of Proof About a Moving Target (Invited Talk). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{andronick:LIPIcs.ITP.2019.1, author = {Andronick, June}, title = {{A Million Lines of Proof About a Moving Target}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {1:1--1:1}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.1}, URN = {urn:nbn:de:0030-drops-110567}, doi = {10.4230/LIPIcs.ITP.2019.1}, annote = {Keywords: Proof maintentance, proof evolution, seL4, Isabelle/HOL} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Kevin Buzzard. What Makes a Mathematician Tick? (Invited Talk). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{buzzard:LIPIcs.ITP.2019.2, author = {Buzzard, Kevin}, title = {{What Makes a Mathematician Tick?}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {2:1--2:1}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.2}, URN = {urn:nbn:de:0030-drops-110576}, doi = {10.4230/LIPIcs.ITP.2019.2}, annote = {Keywords: Formalization of mathematics} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Martin Dixon. An Increasing Need for Formality (Invited Talk). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, p. 3:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{dixon:LIPIcs.ITP.2019.3, author = {Dixon, Martin}, title = {{An Increasing Need for Formality}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {3:1--3:1}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.3}, URN = {urn:nbn:de:0030-drops-110588}, doi = {10.4230/LIPIcs.ITP.2019.3}, annote = {Keywords: Hardware security, formal modeling, instruction sets, SoC’s, negative space testing} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Mohammad Abdulaziz, Charles Gretton, and Michael Norrish. A Verified Compositional Algorithm for AI Planning. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{abdulaziz_et_al:LIPIcs.ITP.2019.4, author = {Abdulaziz, Mohammad and Gretton, Charles and Norrish, Michael}, title = {{A Verified Compositional Algorithm for AI Planning}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {4:1--4: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.4}, URN = {urn:nbn:de:0030-drops-110596}, doi = {10.4230/LIPIcs.ITP.2019.4}, annote = {Keywords: AI Planning, Compositional Algorithms, Algorithm Verification, Transition Systems} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, and Kazunari Tanaka. Proving Tree Algorithms for Succinct Data Structures. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{affeldt_et_al:LIPIcs.ITP.2019.5, author = {Affeldt, Reynald and Garrigue, Jacques and Qi, Xuanrui and Tanaka, Kazunari}, title = {{Proving Tree Algorithms for Succinct Data Structures}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {5:1--5: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.5}, URN = {urn:nbn:de:0030-drops-110609}, doi = {10.4230/LIPIcs.ITP.2019.5}, annote = {Keywords: Coq, small-scale reflection, succinct data structures, LOUDS, bit vectors, self balancing trees} }
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-dev.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)
Guillaume Bertholon, Érik Martin-Dorel, and Pierre Roux. Primitive Floats in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{bertholon_et_al:LIPIcs.ITP.2019.7, author = {Bertholon, Guillaume and Martin-Dorel, \'{E}rik and Roux, Pierre}, title = {{Primitive Floats in Coq}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {7:1--7:20}, 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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.7}, URN = {urn:nbn:de:0030-drops-110629}, doi = {10.4230/LIPIcs.ITP.2019.7}, annote = {Keywords: Coq formal proofs, floating-point arithmetic, reflexive tactics, Cholesky decomposition} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Florent Bréhard, Assia Mahboubi, and Damien Pous. A Certificate-Based Approach to Formally Verified Approximations. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 8:1-8:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{brehard_et_al:LIPIcs.ITP.2019.8, author = {Br\'{e}hard, Florent and Mahboubi, Assia and Pous, Damien}, title = {{A Certificate-Based Approach to Formally Verified Approximations}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {8:1--8: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.8}, URN = {urn:nbn:de:0030-drops-110638}, doi = {10.4230/LIPIcs.ITP.2019.8}, annote = {Keywords: approximation theory, Chebyshev polynomials, Banach fixed-point theorem, interval arithmetic, Coq} }
Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)
Chad E. Brown, Cezary Kaliszyk, and Karol Pąk. Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{brown_et_al:LIPIcs.ITP.2019.9, author = {Brown, Chad E. and Kaliszyk, Cezary and P\k{a}k, Karol}, title = {{Higher-Order Tarski Grothendieck as a Foundation for Formal Proof}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {9:1--9: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.9}, URN = {urn:nbn:de:0030-drops-110643}, doi = {10.4230/LIPIcs.ITP.2019.9}, annote = {Keywords: model, higher-order, Tarski Grothendieck, proof foundation} }
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-dev.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 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-dev.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} }
Feedback for Dagstuhl Publishing