![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Search dblp for Publications
export results for "toc:db/conf/itp/itp2019.bht:"
@inproceedings{DBLP:conf/itp/000119, author = {Lukasz Czajka}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {First-Order Guarded Coinduction in Coq}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {14:1--14:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.14}, doi = {10.4230/LIPICS.ITP.2019.14}, timestamp = {Wed, 21 Aug 2024 22:46:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/000119.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/0001SS19, author = {Julian Brunner and Benedikt Seidl and Salomon Sickert}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {A Verified and Compositional Translation of {LTL} to Deterministic Rabin Automata}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {11:1--11:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.11}, doi = {10.4230/LIPICS.ITP.2019.11}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/0001SS19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/0002D19, author = {Akihisa Yamada and J{\'{e}}r{\'{e}}my Dubut}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Complete Non-Orders and Fixed Points}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {30:1--30:16}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.30}, doi = {10.4230/LIPICS.ITP.2019.30}, timestamp = {Sat, 05 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/0002D19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/0002K19, author = {Yannick Forster and Fabian Kunze}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, 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, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {17:1--17:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.17}, doi = {10.4230/LIPICS.ITP.2019.17}, timestamp = {Sat, 05 Sep 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/0002K19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/AbdulazizGN19, author = {Mohammad Abdulaziz and Charles Gretton and Michael Norrish}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {A Verified Compositional Algorithm for {AI} Planning}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {4:1--4:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.4}, doi = {10.4230/LIPICS.ITP.2019.4}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/AbdulazizGN19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/AffeldtGQT19, author = {Reynald Affeldt and Jacques Garrigue and Xuanrui Qi and Kazunari Tanaka}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Proving Tree Algorithms for Succinct Data Structures}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {5:1--5:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.5}, doi = {10.4230/LIPICS.ITP.2019.5}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/AffeldtGQT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Andronick19, author = {June Andronick}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {A Million Lines of Proof About a Moving Target (Invited Talk)}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {1:1--1:1}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.1}, doi = {10.4230/LIPICS.ITP.2019.1}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Andronick19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/AvigadCH19, author = {Jeremy Avigad and Mario Carneiro and Simon Hudon}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Data Types as Quotients of Polynomial Functors}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {6:1--6:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.6}, doi = {10.4230/LIPICS.ITP.2019.6}, timestamp = {Thu, 25 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/itp/AvigadCH19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/BayerDPSS19, author = {Jonas Bayer and Marco David and Abhik Pal and Benedikt Stock and Dierk Schleicher}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {The {DPRM} Theorem in Isabelle (Short Paper)}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {33:1--33:7}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.33}, doi = {10.4230/LIPICS.ITP.2019.33}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/BayerDPSS19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/BertholonMR19, author = {Guillaume Bertholon and {\'{E}}rik Martin{-}Dorel and Pierre Roux}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Primitive Floats in Coq}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {7:1--7:20}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.7}, doi = {10.4230/LIPICS.ITP.2019.7}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/BertholonMR19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/BrehardMP19, author = {Florent Br{\'{e}}hard and Assia Mahboubi and Damien Pous}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {A Certificate-Based Approach to Formally Verified Approximations}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {8:1--8:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.8}, doi = {10.4230/LIPICS.ITP.2019.8}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/BrehardMP19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/BrownKP19, author = {Chad E. Brown and Cezary Kaliszyk and Karol Pak}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Higher-Order Tarski Grothendieck as a Foundation for Formal Proof}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {9:1--9:16}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.9}, doi = {10.4230/LIPICS.ITP.2019.9}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/BrownKP19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/BrunT19, author = {Matthias Brun and Dmitriy Traytel}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Generic Authenticated Data Structures, Formally}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {10:1--10:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.10}, doi = {10.4230/LIPICS.ITP.2019.10}, timestamp = {Fri, 01 Nov 2019 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/itp/BrunT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Buzzard19, author = {Kevin Buzzard}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {What Makes a Mathematician Tick? (Invited Talk)}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {2:1--2:1}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.2}, doi = {10.4230/LIPICS.ITP.2019.2}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Buzzard19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Carneiro19, author = {Mario Carneiro}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Formalizing Computability Theory via Partial Recursive Functions}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {12:1--12:17}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.12}, doi = {10.4230/LIPICS.ITP.2019.12}, timestamp = {Thu, 25 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/itp/Carneiro19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/ChenCLMT19, author = {Ran Chen and Cyril Cohen and Jean{-}Jacques L{\'{e}}vy and Stephan Merz and Laurent Th{\'{e}}ry}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, 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, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {13:1--13:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.13}, doi = {10.4230/LIPICS.ITP.2019.13}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/ChenCLMT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/DahmenHL19, author = {Sander R. Dahmen and Johannes H{\"{o}}lzl and Robert Y. Lewis}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Formalizing the Solution to the Cap Set Problem}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {15:1--15:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.15}, doi = {10.4230/LIPICS.ITP.2019.15}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/DahmenHL19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Dixon19, author = {Martin Dixon}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {An Increasing Need for Formality (Invited Talk)}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {3:1--3:1}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.3}, doi = {10.4230/LIPICS.ITP.2019.3}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Dixon19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Eberl19, author = {Manuel Eberl}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Nine Chapters of Analytic Number Theory in Isabelle/HOL}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {16:1--16:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.16}, doi = {10.4230/LIPICS.ITP.2019.16}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Eberl19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/GueneauJCP19, author = {Arma{\"{e}}l Gu{\'{e}}neau and Jacques{-}Henri Jourdan and Arthur Chargu{\'{e}}raud and Fran{\c{c}}ois Pottier}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Formal Proof and Analysis of an Incremental Cycle Detection Algorithm}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {18:1--18:20}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.18}, doi = {10.4230/LIPICS.ITP.2019.18}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/GueneauJCP19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/HanD19, author = {Jesse Michael Han and Floris van Doorn}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {A Formalization of Forcing and the Unprovability of the Continuum Hypothesis}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {19:1--19:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.19}, doi = {10.4230/LIPICS.ITP.2019.19}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/HanD19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/HaslbeckL19, author = {Maximilian P. L. Haslbeck and Peter Lammich}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Refinement with Time - Refining the Run-Time of Algorithms in Isabelle/HOL}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {20:1--20:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.20}, doi = {10.4230/LIPICS.ITP.2019.20}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/HaslbeckL19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/ImmlerRW19, author = {Fabian Immler and Jonas R{\"{a}}dle and Makarius Wenzel}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Virtualization of {HOL4} in Isabelle}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {21:1--21:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.21}, doi = {10.4230/LIPICS.ITP.2019.21}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/ImmlerRW19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/JakubuvU19, author = {Jan Jakubuv and Josef Urban}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Hammering Mizar by Learning Clause Guidance (Short Paper)}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {34:1--34:8}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.34}, doi = {10.4230/LIPICS.ITP.2019.34}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/JakubuvU19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/KaliszykP19, author = {Cezary Kaliszyk and Karol Pak}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Declarative Proof Translation (Short Paper)}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {35:1--35:7}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.35}, doi = {10.4230/LIPICS.ITP.2019.35}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/KaliszykP19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Lammich19, author = {Peter Lammich}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Generating Verified {LLVM} from Isabelle/HOL}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {22:1--22:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.22}, doi = {10.4230/LIPICS.ITP.2019.22}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Lammich19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/LammichN19, author = {Peter Lammich and Tobias Nipkow}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, 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, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {23:1--23:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.23}, doi = {10.4230/LIPICS.ITP.2019.23}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/LammichN19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/LasserCFR19, author = {Sam Lasser and Chris Casinghino and Kathleen Fisher and Cody Roux}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {A Verified {LL(1)} Parser Generator}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {24:1--24:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.24}, doi = {10.4230/LIPICS.ITP.2019.24}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/LasserCFR19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/MehtaC19, author = {Mihir Parang Mehta and William R. Cook}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Binary-Compatible Verification of Filesystems with {ACL2}}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {25:1--25:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.25}, doi = {10.4230/LIPICS.ITP.2019.25}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/MehtaC19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/PohjolaRM19, author = {Johannes {\AA}man Pohjola and Henrik Rostedt and Magnus O. Myreen}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {32:1--32:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.32}, doi = {10.4230/LIPICS.ITP.2019.32}, timestamp = {Sun, 02 Oct 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/PohjolaRM19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/RingerYLG19, author = {Talia Ringer and Nathaniel Yazdani and John Leo and Dan Grossman}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Ornaments for Proof Reuse in Coq}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {26:1--26:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.26}, doi = {10.4230/LIPICS.ITP.2019.26}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/RingerYLG19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Severin19, author = {Daniel E. Sever{\'{\i}}n}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Formalization of the Domination Chain with Weighted Parameters (Short Paper)}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {36:1--36:7}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.36}, doi = {10.4230/LIPICS.ITP.2019.36}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Severin19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/SisonM19, author = {Robert Sison and Toby Murray}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Verifying That a Compiler Preserves Concurrent Value-Dependent Information-Flow Security}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {27:1--27:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.27}, doi = {10.4230/LIPICS.ITP.2019.27}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/SisonM19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/SteinbergTT19, author = {Florian Steinberg and Laurent Th{\'{e}}ry and Holger Thies}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Quantitative Continuity and Computable Analysis in Coq}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {28:1--28:21}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.28}, doi = {10.4230/LIPICS.ITP.2019.28}, timestamp = {Mon, 02 Nov 2020 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/itp/SteinbergTT19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Tassi19, author = {Enrico Tassi}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, 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, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {29:1--29:18}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.29}, doi = {10.4230/LIPICS.ITP.2019.29}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Tassi19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/WuG19, author = {Minchao Wu and Rajeev Gor{\'{e}}}, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Verified Decision Procedures for Modal Logics}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {31:1--31:19}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.31}, doi = {10.4230/LIPICS.ITP.2019.31}, timestamp = {Mon, 23 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/WuG19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/X19, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {Front Matter, Table of Contents, Preface, Conference Organization}, booktitle = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, pages = {0:1--0:14}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {https://doi.org/10.4230/LIPIcs.ITP.2019.0}, doi = {10.4230/LIPICS.ITP.2019.0}, timestamp = {Sat, 07 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/X19.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/itp/2019, editor = {John Harrison and John O'Leary and Andrew Tolmach}, title = {10th International Conference on Interactive Theorem Proving, {ITP} 2019, September 9-12, 2019, Portland, OR, {USA}}, series = {LIPIcs}, volume = {141}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2019}, url = {http://www.dagstuhl.de/dagpub/978-3-95977-122-1}, isbn = {978-3-95977-122-1}, timestamp = {Wed, 21 Aug 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/2019.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.