LIPIcs, Volume 141
ITP 2019, September 9-12, 2019, Portland, OR, USA
Editors: John Harrison, John O'Leary, and Andrew Tolmach
Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)
Justin Holmgren and Ron Rothblum. Linear-Size Boolean Circuits for Multiselection. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{holmgren_et_al:LIPIcs.CCC.2024.11, author = {Holmgren, Justin and Rothblum, Ron}, title = {{Linear-Size Boolean Circuits for Multiselection}}, booktitle = {39th Computational Complexity Conference (CCC 2024)}, pages = {11:1--11:20}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-331-7}, ISSN = {1868-8969}, year = {2024}, volume = {300}, editor = {Santhanam, Rahul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.11}, URN = {urn:nbn:de:0030-drops-204070}, doi = {10.4230/LIPIcs.CCC.2024.11}, annote = {Keywords: Private Information Retrieval, Batch Selection, Boolean Circuits} }
Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)
Benoît Guillemet, Assia Mahboubi, and Matthieu Piquerez. Machine-Checked Categorical Diagrammatic Reasoning. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@InProceedings{guillemet_et_al:LIPIcs.FSCD.2024.7, author = {Guillemet, Beno\^{i}t and Mahboubi, Assia and Piquerez, Matthieu}, title = {{Machine-Checked Categorical Diagrammatic Reasoning}}, booktitle = {9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)}, pages = {7:1--7:19}, 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.7}, URN = {urn:nbn:de:0030-drops-203363}, doi = {10.4230/LIPIcs.FSCD.2024.7}, annote = {Keywords: Interactive theorem proving, categories, diagrams, formal proof automation} }
Published in: Dagstuhl Manifestos, Volume 10, Issue 1 (2024)
James P. Delgrande, Birte Glimm, Thomas Meyer, Miroslaw Truszczynski, and Frank Wolter. Current and Future Challenges in Knowledge Representation and Reasoning (Dagstuhl Perspectives Workshop 22282). In Dagstuhl Manifestos, Volume 10, Issue 1, pp. 1-61, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
@Article{delgrande_et_al:DagMan.10.1.1, author = {Delgrande, James P. and Glimm, Birte and Meyer, Thomas and Truszczynski, Miroslaw and Wolter, Frank}, title = {{Current and Future Challenges in Knowledge Representation and Reasoning (Dagstuhl Perspectives Workshop 22282)}}, pages = {1--61}, journal = {Dagstuhl Manifestos}, ISSN = {2193-2433}, year = {2024}, volume = {10}, number = {1}, editor = {Delgrande, James P. and Glimm, Birte and Meyer, Thomas and Truszczynski, Miroslaw and Wolter, Frank}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagMan.10.1.1}, URN = {urn:nbn:de:0030-drops-201403}, doi = {10.4230/DagMan.10.1.1}, annote = {Keywords: Knowledge representation and reasoning, Applications of logics, Declarative representations, Formal logic} }
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 237, 13th International Conference on Interactive Theorem Proving (ITP 2022)
Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin. Dandelion: Certified Approximations of Elementary Functions. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
@InProceedings{becker_et_al:LIPIcs.ITP.2022.6, author = {Becker, Heiko and Tekriwal, Mohit and Darulova, Eva and Volkova, Anastasia and Jeannin, Jean-Baptiste}, title = {{Dandelion: Certified Approximations of Elementary Functions}}, booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)}, pages = {6:1--6:19}, 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.6}, URN = {urn:nbn:de:0030-drops-167155}, doi = {10.4230/LIPIcs.ITP.2022.6}, annote = {Keywords: elementary functions, approximation, certificate checking} }
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.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.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.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.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.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.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.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.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.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} }