Search dblp for Publications

export results for "toc:db/conf/itp/itp2019.bht:"

 download as .bib file

@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}
}
a service of  Schloss Dagstuhl - Leibniz Center for Informatics

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.