Search dblp for Publications

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

 download as .bib file

@inproceedings{DBLP:conf/itp/0002D23,
  author       = {Akihisa Yamada and
                  J{\'{e}}r{\'{e}}my Dubut},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Formalizing Results on Directed Sets in Isabelle/HOL (Proof Pearl)},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {34:1--34:13},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.34},
  doi          = {10.4230/LIPICS.ITP.2023.34},
  timestamp    = {Wed, 26 Jul 2023 16:07:09 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/0002D23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/AbdulazizM23,
  author       = {Mohammad Abdulaziz and
                  Christoph Madlener},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {A Formal Analysis of {RANKING}},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {3:1--3:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.3},
  doi          = {10.4230/LIPICS.ITP.2023.3},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/AbdulazizM23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/AbrahamssonM23,
  author       = {Oskar Abrahamsson and
                  Magnus O. Myreen},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Fast, Verified Computation for Candle},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {4:1--4:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.4},
  doi          = {10.4230/LIPICS.ITP.2023.4},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/AbrahamssonM23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/AccattoliBC23,
  author       = {Beniamino Accattoli and
                  Horace Blanc and
                  Claudio Sacerdoti Coen},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Formalizing Functions as Processes},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {5:1--5:21},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.5},
  doi          = {10.4230/LIPICS.ITP.2023.5},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/AccattoliBC23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/AngdinataX23,
  author       = {David Kurniadi Angdinata and
                  Junyan Xu},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {An Elementary Formal Proof of the Group Law on Weierstrass Elliptic
                  Curves in Any Characteristic},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {6:1--6:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.6},
  doi          = {10.4230/LIPICS.ITP.2023.6},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/AngdinataX23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/AvigadGLST23,
  author       = {Jeremy Avigad and
                  Lior Goldberg and
                  David Levit and
                  Yoav Seginer and
                  Alon Titelman},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {A Proof-Producing Compiler for Blockchain Applications},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {7:1--7:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.7},
  doi          = {10.4230/LIPICS.ITP.2023.7},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/AvigadGLST23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BestBBB23,
  author       = {Alex J. Best and
                  Christopher Birkbeck and
                  Riccardo Brasca and
                  Eric Rodriguez Boidi},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Fermat's Last Theorem for Regular Primes (Short Paper)},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {36:1--36:8},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.36},
  doi          = {10.4230/LIPICS.ITP.2023.36},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/BestBBB23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BorgesAFAMPSZ23,
  author       = {Ana de Almeida Borges and
                  Annal{\'{\i}} Casanueva Art{\'{\i}}s and
                  Jean{-}R{\'{e}}my Falleri and
                  Emilio Jes{\'{u}}s Gallego Arias and
                  {\'{E}}rik Martin{-}Dorel and
                  Karl Palmskog and
                  Alexander Serebrenik and
                  Th{\'{e}}o Zimmermann},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Lessons for Interactive Theorem Proving Researchers from a Survey
                  of Coq Users},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {12:1--12:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.12},
  doi          = {10.4230/LIPICS.ITP.2023.12},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/BorgesAFAMPSZ23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BosmanKS23,
  author       = {Roger Bosman and
                  Georgios Karachalias and
                  Tom Schrijvers},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {No Unification Variable Left Behind: Fully Grounding Type Inference
                  for the {HDM} System},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {8:1--8:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.8},
  doi          = {10.4230/LIPICS.ITP.2023.8},
  timestamp    = {Sun, 12 Nov 2023 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/BosmanKS23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Carneiro23,
  author       = {Mario Carneiro},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Reimplementing Mizar in Rust},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {10:1--10:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.10},
  doi          = {10.4230/LIPICS.ITP.2023.10},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Carneiro23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/CarneiroBU23,
  author       = {Mario Carneiro and
                  Chad E. Brown and
                  Josef Urban},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Automated Theorem Proving for Metamath},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {9:1--9:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.9},
  doi          = {10.4230/LIPICS.ITP.2023.9},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/CarneiroBU23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Cruz-FilipeM23,
  author       = {Lu{\'{\i}}s Cruz{-}Filipe and
                  Fabrizio Montesi},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Now It Compiles! Certified Automatic Repair of Uncompilable Protocols},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {11:1--11:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.11},
  doi          = {10.4230/LIPICS.ITP.2023.11},
  timestamp    = {Sat, 30 Sep 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Cruz-FilipeM23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/DunnTZ23,
  author       = {Lawrence Dunn and
                  Val Tannen and
                  Steve Zdancewic},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Tealeaves: Structured Monads for Generic First-Order Abstract Syntax
                  Infrastructure},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {14:1--14:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.14},
  doi          = {10.4230/LIPICS.ITP.2023.14},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/DunnTZ23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/DvorakB23,
  author       = {Martin Dvorak and
                  Jasmin Blanchette},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Closure Properties of General Grammars - Formally Verified},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {15:1--15:16},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.15},
  doi          = {10.4230/LIPICS.ITP.2023.15},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/DvorakB23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Flaten23,
  author       = {Jarl G. Taxer{\aa}s Flaten},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Formalising Yoneda Ext in Univalent Foundations},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {16:1--16:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.16},
  doi          = {10.4230/LIPICS.ITP.2023.16},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Flaten23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Frutos-Fernandez23,
  author       = {Mar{\'{\i}}a In{\'{e}}s de Frutos{-}Fern{\'{a}}ndez},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Formalizing Norm Extensions and Applications to Number Theory},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {13:1--13:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.13},
  doi          = {10.4230/LIPICS.ITP.2023.13},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Frutos-Fernandez23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/GrabowskiK23,
  author       = {Adam Grabowski and
                  Artur Kornilowicz},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Implementing More Explicit Definitional Expansions in Mizar (Short
                  Paper)},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {37:1--37:8},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.37},
  doi          = {10.4230/LIPICS.ITP.2023.37},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/GrabowskiK23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/GuilloudGK23,
  author       = {Simon Guilloud and
                  Sankalp Gambhir and
                  Viktor Kuncak},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {{LISA} - {A} Modern Proof System},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {17:1--17:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.17},
  doi          = {10.4230/LIPICS.ITP.2023.17},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/GuilloudGK23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/HirataM023,
  author       = {Michikazu Hirata and
                  Yasuhiko Minamide and
                  Tetsuya Sato},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {18:1--18:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.18},
  doi          = {10.4230/LIPICS.ITP.2023.18},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/HirataM023.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/JakubuvCGKOP00U23,
  author       = {Jan Jakubuv and
                  Karel Chvalovsk{\'{y}} and
                  Zarathustra Amadeus Goertzel and
                  Cezary Kaliszyk and
                  Mirek Ols{\'{a}}k and
                  Bartosz Piotrowski and
                  Stephan Schulz and
                  Martin Suda and
                  Josef Urban},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {MizAR 60 for Mizar 50},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {19:1--19:22},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.19},
  doi          = {10.4230/LIPICS.ITP.2023.19},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/JakubuvCGKOP00U23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/JoramV23,
  author       = {Philipp Joram and
                  Niccol{\`{o}} Veltri},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Constructive Final Semantics of Finite Bags},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {20:1--20:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.20},
  doi          = {10.4230/LIPICS.ITP.2023.20},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/JoramV23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/KohlM23,
  author       = {Christina Kohl and
                  Aart Middeldorp},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Formalizing Almost Development Closed Critical Pairs (Short Paper)},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {38:1--38:8},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.38},
  doi          = {10.4230/LIPICS.ITP.2023.38},
  timestamp    = {Sun, 12 Nov 2023 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/KohlM23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Koutsoukou-Argyraki23,
  author       = {Angeliki Koutsoukou{-}Argyraki},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Formalisation of Additive Combinatorics in Isabelle/HOL (Invited Talk)},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {1:1--1:2},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.1},
  doi          = {10.4230/LIPICS.ITP.2023.1},
  timestamp    = {Sun, 12 Nov 2023 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/Koutsoukou-Argyraki23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Krebbers23,
  author       = {Robbert Krebbers},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Interactive and Automated Proofs in Modal Separation Logic (Invited
                  Talk)},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {2:1--2:1},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.2},
  doi          = {10.4230/LIPICS.ITP.2023.2},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Krebbers23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Larchey-Wendling23,
  author       = {Dominique Larchey{-}Wendling and
                  Jean{-}Fran{\c{c}}ois Monin},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Proof Pearl: Faithful Computation and Extraction of {\(\mu\)}-Recursive
                  Algorithms in Coq},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {21:1--21:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.21},
  doi          = {10.4230/LIPICS.ITP.2023.21},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Larchey-Wendling23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Livingston23,
  author       = {Amelia Livingston},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Group Cohomology in the Lean Community Library},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {22:1--22:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.22},
  doi          = {10.4230/LIPICS.ITP.2023.22},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Livingston23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Nash23,
  author       = {Oliver Nash},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {A Formalisation of Gallagher's Ergodic Theorem},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {23:1--23:16},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.23},
  doi          = {10.4230/LIPICS.ITP.2023.23},
  timestamp    = {Sun, 12 Nov 2023 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/Nash23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/NawrockiAE23,
  author       = {Wojciech Nawrocki and
                  Edward W. Ayers and
                  Gabriel Ebner},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {An Extensible User Interface for Lean 4},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {24:1--24:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.24},
  doi          = {10.4230/LIPICS.ITP.2023.24},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/NawrockiAE23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Pomeret-CoquotF23,
  author       = {Pierre Pomeret{-}Coquot and
                  H{\'{e}}l{\`{e}}ne Fargier and
                  {\'{E}}rik Martin{-}Dorel},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Bel-Games: {A} Formal Theory of Games of Incomplete Information Based
                  on Belief Functions in the Coq Proof Assistant},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {25:1--25:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.25},
  doi          = {10.4230/LIPICS.ITP.2023.25},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Pomeret-CoquotF23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/ReichelHTGR23,
  author       = {Tom Reichel and
                  R. Wesley Henderson and
                  Andrew Touchet and
                  Andrew Gardner and
                  Talia Ringer},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Proof Repair Infrastructure for Supervised Models: Building a Large
                  Proof Repair Dataset},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {26:1--26:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.26},
  doi          = {10.4230/LIPICS.ITP.2023.26},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/ReichelHTGR23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/TanU23,
  author       = {Chengsong Tan and
                  Christian Urban},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {{POSIX} Lexing with Bitcoded Derivatives},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {27:1--27:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.27},
  doi          = {10.4230/LIPICS.ITP.2023.27},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/TanU23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/TiroreBC23,
  author       = {Dawit Legesse Tirore and
                  Jesper Bengtson and
                  Marco Carbone},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {A Sound and Complete Projection for Global Types},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {28:1--28:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.28},
  doi          = {10.4230/LIPICS.ITP.2023.28},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/TiroreBC23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/TothN23,
  author       = {Bal{\'{a}}zs T{\'{o}}th and
                  Tobias Nipkow},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Real-Time Double-Ended Queue Verified (Proof Pearl)},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {29:1--29:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.29},
  doi          = {10.4230/LIPICS.ITP.2023.29},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/TothN23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Voorneveld23,
  author       = {Niels F. W. Voorneveld},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Slice Nondeterminism},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {31:1--31:19},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.31},
  doi          = {10.4230/LIPICS.ITP.2023.31},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Voorneveld23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/WangPWDBA23,
  author       = {Qinshi Wang and
                  Mengying Pan and
                  Shengyi Wang and
                  Ryan Doenges and
                  Lennart Beringer and
                  Andrew W. Appel},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Foundational Verification of Stateful {P4} Packet Processing},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {32:1--32:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.32},
  doi          = {10.4230/LIPICS.ITP.2023.32},
  timestamp    = {Mon, 05 Feb 2024 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/WangPWDBA23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/WeideVK23,
  author       = {Niels van der Weide and
                  Deivid Vale and
                  Cynthia Kop},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Certifying Higher-Order Polynomial Interpretations},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {30:1--30:20},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.30},
  doi          = {10.4230/LIPICS.ITP.2023.30},
  timestamp    = {Tue, 07 May 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/WeideVK23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/X23,
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Front Matter, Table of Contents, Preface, Conference Organization},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {0:1--0:10},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.0},
  doi          = {10.4230/LIPICS.ITP.2023.0},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/X23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/XuN23,
  author       = {Yiming Xu and
                  Michael Norrish},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Dependently Sorted Theorem Proving for Mathematical Foundations},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {33:1--33:18},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.33},
  doi          = {10.4230/LIPICS.ITP.2023.33},
  timestamp    = {Sat, 30 Sep 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/XuN23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Zhang23,
  author       = {Jujian Zhang},
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {Formalising the Proj Construction in Lean},
  booktitle    = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  pages        = {35:1--35:17},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://doi.org/10.4230/LIPIcs.ITP.2023.35},
  doi          = {10.4230/LIPICS.ITP.2023.35},
  timestamp    = {Tue, 07 May 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Zhang23.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/itp/2023,
  editor       = {Adam Naumowicz and
                  Ren{\'{e}} Thiemann},
  title        = {14th International Conference on Interactive Theorem Proving, {ITP}
                  2023, July 31 to August 4, 2023, Bia{\l}ystok, Poland},
  series       = {LIPIcs},
  volume       = {268},
  publisher    = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
  year         = {2023},
  url          = {https://www.dagstuhl.de/dagpub/978-3-95977-284-6},
  isbn         = {978-3-95977-284-6},
  timestamp    = {Wed, 26 Jul 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/2023.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.