@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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-dev.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}
}
@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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
@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-dev.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}
}
The metadata provided by Dagstuhl Publishing on its webpages, as well as their export formats (such as XML or BibTeX) available at our website, is released under the CC0 1.0 Public Domain Dedication license. That is, you are free to copy, distribute, use, modify, transform, build upon, and produce derived works from our data, even for commercial purposes, all without asking permission. Of course, we are always happy if you provide a link to us as the source of the data.
Read the full CC0 1.0 legal code for the exact terms that apply: https://creativecommons.org/publicdomain/zero/1.0/legalcode
Feedback for Dagstuhl Publishing