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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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} }
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.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} }
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.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} }
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} }
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} }
Mario Carneiro. Formalizing Computability Theory via Partial Recursive Functions. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{carneiro:LIPIcs.ITP.2019.12, author = {Carneiro, Mario}, title = {{Formalizing Computability Theory via Partial Recursive Functions}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {12:1--12:17}, 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.12}, URN = {urn:nbn:de:0030-drops-110671}, doi = {10.4230/LIPIcs.ITP.2019.12}, annote = {Keywords: Lean, computability, halting problem, primitive recursion} }
Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, and Laurent Théry. Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{chen_et_al:LIPIcs.ITP.2019.13, author = {Chen, Ran and Cohen, Cyril and L\'{e}vy, Jean-Jacques and Merz, Stephan and Th\'{e}ry, Laurent}, title = {{Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {13:1--13: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.13}, URN = {urn:nbn:de:0030-drops-110683}, doi = {10.4230/LIPIcs.ITP.2019.13}, annote = {Keywords: Mathematical logic, Formal proof, Graph algorithm, Program verification} }
Łukasz Czajka. First-Order Guarded Coinduction in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{czajka:LIPIcs.ITP.2019.14, author = {Czajka, {\L}ukasz}, title = {{First-Order Guarded Coinduction in Coq}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {14:1--14: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.14}, URN = {urn:nbn:de:0030-drops-110690}, doi = {10.4230/LIPIcs.ITP.2019.14}, annote = {Keywords: coinduction, Coq, guardedness, corecursion} }
Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. Formalizing the Solution to the Cap Set Problem. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 15:1-15:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{dahmen_et_al:LIPIcs.ITP.2019.15, author = {Dahmen, Sander R. and H\"{o}lzl, Johannes and Lewis, Robert Y.}, title = {{Formalizing the Solution to the Cap Set Problem}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {15:1--15: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.15}, URN = {urn:nbn:de:0030-drops-110703}, doi = {10.4230/LIPIcs.ITP.2019.15}, annote = {Keywords: formal proof, combinatorics, cap set problem, Lean} }
Manuel Eberl. Nine Chapters of Analytic Number Theory in Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 16:1-16:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{eberl:LIPIcs.ITP.2019.16, author = {Eberl, Manuel}, title = {{Nine Chapters of Analytic Number Theory in Isabelle/HOL}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {16:1--16: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.16}, URN = {urn:nbn:de:0030-drops-110714}, doi = {10.4230/LIPIcs.ITP.2019.16}, annote = {Keywords: Isabelle, theorem proving, analytic number theory, number theory, arithmetical function, Dirichlet series, prime number theorem, Dirichlet’s theorem, zeta function, L functions} }
Yannick Forster and Fabian Kunze. A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 17:1-17:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{forster_et_al:LIPIcs.ITP.2019.17, author = {Forster, Yannick and Kunze, Fabian}, title = {{A Certifying Extraction with Time Bounds from Coq to Call-By-Value Lambda Calculus}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {17:1--17: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.17}, URN = {urn:nbn:de:0030-drops-110724}, doi = {10.4230/LIPIcs.ITP.2019.17}, annote = {Keywords: call-by-value, lambda calculus, Coq, constructive type theory, extraction, computability} }
Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{gueneau_et_al:LIPIcs.ITP.2019.18, author = {Gu\'{e}neau, Arma\"{e}l and Jourdan, Jacques-Henri and Chargu\'{e}raud, Arthur and Pottier, Fran\c{c}ois}, title = {{Formal Proof and Analysis of an Incremental Cycle Detection Algorithm}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {18:1--18: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.18}, URN = {urn:nbn:de:0030-drops-110739}, doi = {10.4230/LIPIcs.ITP.2019.18}, annote = {Keywords: interactive deductive program verification, complexity analysis} }
Jesse Michael Han and Floris van Doorn. A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 19:1-19:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{han_et_al:LIPIcs.ITP.2019.19, author = {Han, Jesse Michael and van Doorn, Floris}, title = {{A Formalization of Forcing and the Unprovability of the Continuum Hypothesis}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {19:1--19: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.19}, URN = {urn:nbn:de:0030-drops-110742}, doi = {10.4230/LIPIcs.ITP.2019.19}, annote = {Keywords: Interactive theorem proving, formal verification, set theory, forcing, independence proofs, continuum hypothesis, Boolean-valued models, Lean} }
Maximilian P. L. Haslbeck and Peter Lammich. Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{haslbeck_et_al:LIPIcs.ITP.2019.20, author = {Haslbeck, Maximilian P. L. and Lammich, Peter}, title = {{Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {20:1--20: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.20}, URN = {urn:nbn:de:0030-drops-110754}, doi = {10.4230/LIPIcs.ITP.2019.20}, annote = {Keywords: Isabelle, Time Complexity Analysis, Separation Logic, Program Verification, Refinement, Run Time, Algorithms} }
Fabian Immler, Jonas Rädle, and Makarius Wenzel. Virtualization of HOL4 in Isabelle. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{immler_et_al:LIPIcs.ITP.2019.21, author = {Immler, Fabian and R\"{a}dle, Jonas and Wenzel, Makarius}, title = {{Virtualization of HOL4 in Isabelle}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {21:1--21: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.21}, URN = {urn:nbn:de:0030-drops-110760}, doi = {10.4230/LIPIcs.ITP.2019.21}, annote = {Keywords: Virtualization, HOL4, Isabelle, Isabelle/HOL, Isabelle/ML} }
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} }
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} }
Sam Lasser, Chris Casinghino, Kathleen Fisher, and Cody Roux. A Verified LL(1) Parser Generator. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{lasser_et_al:LIPIcs.ITP.2019.24, author = {Lasser, Sam and Casinghino, Chris and Fisher, Kathleen and Roux, Cody}, title = {{A Verified LL(1) Parser Generator}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {24:1--24: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.24}, URN = {urn:nbn:de:0030-drops-110794}, doi = {10.4230/LIPIcs.ITP.2019.24}, annote = {Keywords: interactive theorem proving, top-down parsing} }
Mihir Parang Mehta and William R. Cook. Binary-Compatible Verification of Filesystems with ACL2. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{mehta_et_al:LIPIcs.ITP.2019.25, author = {Mehta, Mihir Parang and Cook, William R.}, title = {{Binary-Compatible Verification of Filesystems with ACL2}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {25:1--25: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.25}, URN = {urn:nbn:de:0030-drops-110807}, doi = {10.4230/LIPIcs.ITP.2019.25}, annote = {Keywords: interactive theorem proving, filesystems} }
Talia Ringer, Nathaniel Yazdani, John Leo, and Dan Grossman. Ornaments for Proof Reuse in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{ringer_et_al:LIPIcs.ITP.2019.26, author = {Ringer, Talia and Yazdani, Nathaniel and Leo, John and Grossman, Dan}, title = {{Ornaments for Proof Reuse in Coq}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {26:1--26: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.26}, URN = {urn:nbn:de:0030-drops-110816}, doi = {10.4230/LIPIcs.ITP.2019.26}, annote = {Keywords: ornaments, proof reuse, proof automation} }
Robert Sison and Toby Murray. Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{sison_et_al:LIPIcs.ITP.2019.27, author = {Sison, Robert and Murray, Toby}, title = {{Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {27:1--27: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.27}, URN = {urn:nbn:de:0030-drops-110829}, doi = {10.4230/LIPIcs.ITP.2019.27}, annote = {Keywords: Secure compilation, Information flow security, Concurrency, Verification} }
Florian Steinberg, Laurent Théry, and Holger Thies. Quantitative Continuity and Computable Analysis in Coq. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{steinberg_et_al:LIPIcs.ITP.2019.28, author = {Steinberg, Florian and Th\'{e}ry, Laurent and Thies, Holger}, title = {{Quantitative Continuity and Computable Analysis in Coq}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {28:1--28:21}, 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.28}, URN = {urn:nbn:de:0030-drops-110830}, doi = {10.4230/LIPIcs.ITP.2019.28}, annote = {Keywords: computable analysis, Coq, contionuous functionals, discontinuity, closed choice on the naturals} }
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} }
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} }
Minchao Wu and Rajeev Goré. Verified Decision Procedures for Modal Logics. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{wu_et_al:LIPIcs.ITP.2019.31, author = {Wu, Minchao and Gor\'{e}, Rajeev}, title = {{Verified Decision Procedures for Modal Logics}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {31:1--31: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.31}, URN = {urn:nbn:de:0030-drops-110866}, doi = {10.4230/LIPIcs.ITP.2019.31}, annote = {Keywords: Formal Methods, Interactive Theorem Proving, Modal Logic, Lean} }
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} }
Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, and Dierk Schleicher. The DPRM Theorem in Isabelle (Short Paper). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 33:1-33:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{bayer_et_al:LIPIcs.ITP.2019.33, author = {Bayer, Jonas and David, Marco and Pal, Abhik and Stock, Benedikt and Schleicher, Dierk}, title = {{The DPRM Theorem in Isabelle}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {33:1--33:7}, 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.33}, URN = {urn:nbn:de:0030-drops-110883}, doi = {10.4230/LIPIcs.ITP.2019.33}, annote = {Keywords: DPRM theorem, Hilbert’s tenth problem, Diophantine predicates, Register machines, Recursively enumerable sets, Isabelle, Formal verification} }
Jan Jakubův and Josef Urban. Hammering Mizar by Learning Clause Guidance (Short Paper). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 34:1-34:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{jakubuv_et_al:LIPIcs.ITP.2019.34, author = {Jakub\r{u}v, Jan and Urban, Josef}, title = {{Hammering Mizar by Learning Clause Guidance}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {34:1--34:8}, 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.34}, URN = {urn:nbn:de:0030-drops-110898}, doi = {10.4230/LIPIcs.ITP.2019.34}, annote = {Keywords: Proof automation, ITP hammers, Automated theorem proving, Machine learning} }
Cezary Kaliszyk and Karol Pąk. Declarative Proof Translation (Short Paper). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 35:1-35:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{kaliszyk_et_al:LIPIcs.ITP.2019.35, author = {Kaliszyk, Cezary and P\k{a}k, Karol}, title = {{Declarative Proof Translation}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {35:1--35:7}, 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.35}, URN = {urn:nbn:de:0030-drops-110903}, doi = {10.4230/LIPIcs.ITP.2019.35}, annote = {Keywords: Declarative Proof, Translation, Isabelle/Isar, Mizar} }
Daniel E. Severín. Formalization of the Domination Chain with Weighted Parameters (Short Paper). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 36:1-36:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
@InProceedings{severin:LIPIcs.ITP.2019.36, author = {Sever{\'\i}n, Daniel E.}, title = {{Formalization of the Domination Chain with Weighted Parameters}}, booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)}, pages = {36:1--36:7}, 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.36}, URN = {urn:nbn:de:0030-drops-110919}, doi = {10.4230/LIPIcs.ITP.2019.36}, annote = {Keywords: Domination Chain, Coq, Formalization of Mathematics} }