Search dblp for Publications

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

 download as .bib file

@inproceedings{DBLP:conf/itp/0002HS18,
  author       = {Yannick Forster and
                  Edith Heiter and
                  Gert Smolka},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Verification of PCP-Related Computational Reductions in Coq},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {253--269},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_15},
  doi          = {10.1007/978-3-319-94821-8\_15},
  timestamp    = {Sat, 05 Sep 2020 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/0002HS18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/AchermannHCR18,
  author       = {Reto Achermann and
                  Lukas Humbel and
                  David A. Cock and
                  Timothy Roscoe},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Physical Addressing on Real Hardware in Isabelle/HOL},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {1--19},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_1},
  doi          = {10.1007/978-3-319-94821-8\_1},
  timestamp    = {Wed, 21 Dec 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/AchermannHCR18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/AnandBCST18,
  author       = {Abhishek Anand and
                  Simon Boulier and
                  Cyril Cohen and
                  Matthieu Sozeau and
                  Nicolas Tabareau},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Towards Certified Meta-Programming with Typed Template-Coq},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {20--39},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_2},
  doi          = {10.1007/978-3-319-94821-8\_2},
  timestamp    = {Sun, 02 Oct 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/AnandBCST18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/AvigadM18,
  author       = {Jeremy Avigad and
                  Assia Mahboubi},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Erratum to: Interactive Theorem Proving},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_38},
  doi          = {10.1007/978-3-319-94821-8\_38},
  timestamp    = {Wed, 03 Oct 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/AvigadM18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BalcoF00P18,
  author       = {Samuel Balco and
                  Sabine Frittella and
                  Giuseppe Greco and
                  Alexander Kurz and
                  Alessandra Palmigiano},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Software Tool Support for Modular Reasoning in Modal Logics of Actions},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {48--67},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_4},
  doi          = {10.1007/978-3-319-94821-8\_4},
  timestamp    = {Mon, 26 Jun 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/BalcoF00P18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BannisterHK18,
  author       = {Callum Bannister and
                  Peter H{\"{o}}fner and
                  Gerwin Klein},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Backwards and Forwards with Separation Logic},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {68--87},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_5},
  doi          = {10.1007/978-3-319-94821-8\_5},
  timestamp    = {Thu, 05 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/BannisterHK18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BastonC18,
  author       = {Colm Baston and
                  Venanzio Capretta},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {The Coinductive Formulation of Common Knowledge},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {126--141},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_8},
  doi          = {10.1007/978-3-319-94821-8\_8},
  timestamp    = {Fri, 02 Nov 2018 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/BastonC18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BenzakenCKM18,
  author       = {V{\'{e}}ronique Benzaken and
                  Evelyne Contejean and
                  Chantal Keller and
                  Eunice Martins},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {A Coq Formalisation of SQL's Execution Engines},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {88--107},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_6},
  doi          = {10.1007/978-3-319-94821-8\_6},
  timestamp    = {Sun, 02 Oct 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/BenzakenCKM18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/BoulmeM18,
  author       = {Sylvain Boulm{\'{e}} and
                  Alexandre Mar{\'{e}}chal},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {A Coq Tactic for Equality Learning in Linear Arithmetic},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {108--125},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_7},
  doi          = {10.1007/978-3-319-94821-8\_7},
  timestamp    = {Thu, 05 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/BoulmeM18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/CaretteFL18,
  author       = {Jacques Carette and
                  William M. Farmer and
                  Patrick Laskowski},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {{HOL} Light {QE}},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {215--234},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_13},
  doi          = {10.1007/978-3-319-94821-8\_13},
  timestamp    = {Thu, 05 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/CaretteFL18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Cauderlier18,
  author       = {Rapha{\"{e}}l Cauderlier},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Tactics and Certificates in Meta Dedukti},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {142--159},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_9},
  doi          = {10.1007/978-3-319-94821-8\_9},
  timestamp    = {Thu, 05 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Cauderlier18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/DivasonJT018,
  author       = {Jose Divas{\'{o}}n and
                  Sebastiaan J. C. Joosten and
                  Ren{\'{e}} Thiemann and
                  Akihisa Yamada},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {A Formalization of the {LLL} Basis Reduction Algorithm},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {160--177},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_10},
  doi          = {10.1007/978-3-319-94821-8\_10},
  timestamp    = {Mon, 15 Jun 2020 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/DivasonJT018.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/DoczkalCP18,
  author       = {Christian Doczkal and
                  Guillaume Combette and
                  Damien Pous},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {178--195},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_11},
  doi          = {10.1007/978-3-319-94821-8\_11},
  timestamp    = {Thu, 05 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/DoczkalCP18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/EberlHN18,
  author       = {Manuel Eberl and
                  Max W. Haslbeck and
                  Tobias Nipkow},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Verified Analysis of Random Binary Tree Structures},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {196--214},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_12},
  doi          = {10.1007/978-3-319-94821-8\_12},
  timestamp    = {Tue, 10 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/EberlHN18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/FirsovBS18,
  author       = {Denis Firsov and
                  Richard Blair and
                  Aaron Stump},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Efficient Mendler-Style Lambda-Encodings in Cedille},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {235--252},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_14},
  doi          = {10.1007/978-3-319-94821-8\_14},
  timestamp    = {Sun, 25 Oct 2020 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/FirsovBS18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/FlorS18,
  author       = {Jo{\~{a}}o Paulo Pizani Flor and
                  Wouter Swierstra},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Verified Timing Transformations in Synchronous Circuits with {\textbackslash}lambda
                  {\textbackslash}pi -Ware},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {504--522},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_30},
  doi          = {10.1007/978-3-319-94821-8\_30},
  timestamp    = {Sat, 30 Sep 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/FlorS18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/GoertzelJ0U18,
  author       = {Zarathustra Amadeus Goertzel and
                  Jan Jakubuv and
                  Stephan Schulz and
                  Josef Urban},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {ProofWatch: Watchlist Guidance for Large Theories in {E}},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {270--288},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_16},
  doi          = {10.1007/978-3-319-94821-8\_16},
  timestamp    = {Sat, 28 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/GoertzelJ0U18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/GrossEC18,
  author       = {Jason Gross and
                  Andres Erbsen and
                  Adam Chlipala},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Reification by Parametricity - Fast Setup for Proof by Reflection,
                  in Two Lines of Ltac},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {289--305},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_17},
  doi          = {10.1007/978-3-319-94821-8\_17},
  timestamp    = {Thu, 05 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/GrossEC18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/JantschN18,
  author       = {Simon Jantsch and
                  Michael Norrish},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Verifying the {LTL} to B{\"{u}}chi Automata Translation via Very
                  Weak Alternating Automata},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {306--323},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_18},
  doi          = {10.1007/978-3-319-94821-8\_18},
  timestamp    = {Wed, 25 Sep 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/JantschN18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Kahl18,
  author       = {Wolfram Kahl},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {CalcCheck: {A} Proof Checker for Teaching the "Logical Approach to
                  Discrete Math"},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {324--341},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_19},
  doi          = {10.1007/978-3-319-94821-8\_19},
  timestamp    = {Thu, 05 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Kahl18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/KnuppelTPS18,
  author       = {Alexander Kn{\"{u}}ppel and
                  Thomas Th{\"{u}}m and
                  Carsten Immanuel Pardylla and
                  Ina Schaefer},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Understanding Parameters of Deductive Verification: An Empirical Investigation
                  of KeY},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {342--361},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_20},
  doi          = {10.1007/978-3-319-94821-8\_20},
  timestamp    = {Thu, 05 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/KnuppelTPS18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/KumarMTM18,
  author       = {Ramana Kumar and
                  Eric Mullen and
                  Zachary Tatlock and
                  Magnus O. Myreen},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Software Verification with ITPs Should Use Binary Code Extraction
                  to Reduce the {TCB} - (Short Paper)},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {362--369},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_21},
  doi          = {10.1007/978-3-319-94821-8\_21},
  timestamp    = {Sun, 12 Feb 2023 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/KumarMTM18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Larchey-Wendling18,
  author       = {Dominique Larchey{-}Wendling},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Proof Pearl: Constructive Extraction of Cycle Finding Algorithms},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {370--387},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_22},
  doi          = {10.1007/978-3-319-94821-8\_22},
  timestamp    = {Mon, 16 Sep 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Larchey-Wendling18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Lochbihler18,
  author       = {Andreas Lochbihler},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Fast Machine Words in Isabelle/HOL},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {388--410},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_23},
  doi          = {10.1007/978-3-319-94821-8\_23},
  timestamp    = {Thu, 05 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Lochbihler18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/LochbihlerS18,
  author       = {Andreas Lochbihler and
                  Joshua Schneider},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Relational Parametricity and Quotient Preservation for Modular (Co)datatypes},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {411--431},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_24},
  doi          = {10.1007/978-3-319-94821-8\_24},
  timestamp    = {Tue, 17 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/LochbihlerS18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/MendesF18,
  author       = {Alexandra Mendes and
                  Jo{\~{a}}o F. Ferreira},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Towards Verified Handwritten Calculational Proofs - (Short Paper)},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {432--440},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_25},
  doi          = {10.1007/978-3-319-94821-8\_25},
  timestamp    = {Fri, 22 Apr 2022 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/MendesF18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/MessnerPSS18,
  author       = {Florian Me{\ss}ner and
                  Julian Parsert and
                  Jonas Sch{\"{o}}pf and
                  Christian Sternagel},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {A Formally Verified Solver for Homogeneous Linear Diophantine Equations},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {441--458},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_26},
  doi          = {10.1007/978-3-319-94821-8\_26},
  timestamp    = {Sun, 25 Oct 2020 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/MessnerPSS18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Miquey18,
  author       = {{\'{E}}tienne Miquey},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Formalizing Implicative Algebras in Coq},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {459--476},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_27},
  doi          = {10.1007/978-3-319-94821-8\_27},
  timestamp    = {Thu, 23 Sep 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Miquey18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/MoscatoPMF18,
  author       = {Mariano M. Moscato and
                  Carlos Gustavo L{\'{o}}pez Pombo and
                  C{\'{e}}sar A. Mu{\~{n}}oz and
                  Marco A. Feli{\'{u}}},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Boosting the Reuse of Formal Specifications},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {477--494},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_28},
  doi          = {10.1007/978-3-319-94821-8\_28},
  timestamp    = {Thu, 05 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/MoscatoPMF18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/ParsertK18,
  author       = {Julian Parsert and
                  Cezary Kaliszyk},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Towards Formal Foundations for Game Theory},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {495--503},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_29},
  doi          = {10.1007/978-3-319-94821-8\_29},
  timestamp    = {Wed, 16 Mar 2022 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/ParsertK18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/RizkallahGZ18,
  author       = {Christine Rizkallah and
                  Dmitri Garbuzov and
                  Steve Zdancewic},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {A Formal Equational Theory for Call-By-Push-Value},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {523--541},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_31},
  doi          = {10.1007/978-3-319-94821-8\_31},
  timestamp    = {Thu, 14 Oct 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/RizkallahGZ18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/SilvaLG18,
  author       = {Andr{\'{e}}ia B. Avelar da Silva and
                  Thaynara Arielly de Lima and
                  Andr{\'{e}} Luiz Galdino},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Formalizing Ring Theory in {PVS}},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {40--47},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_3},
  doi          = {10.1007/978-3-319-94821-8\_3},
  timestamp    = {Thu, 14 Oct 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/SilvaLG18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/SyedaK18,
  author       = {Hira Taqdees Syeda and
                  Gerwin Klein},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Program Verification in the Presence of Cached Address Translation},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {542--559},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_32},
  doi          = {10.1007/978-3-319-94821-8\_32},
  timestamp    = {Tue, 07 May 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/SyedaK18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/Tassarotti018,
  author       = {Joseph Tassarotti and
                  Robert Harper},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Verified Tail Bounds for Randomized Programs},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {560--578},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_33},
  doi          = {10.1007/978-3-319-94821-8\_33},
  timestamp    = {Thu, 05 Jul 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/Tassarotti018.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/WimmerH18,
  author       = {Simon Wimmer and
                  Johannes H{\"{o}}lzl},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {{MDP} + {TA} = {PTA:} Probabilistic Timed Automata, Formalized (Short
                  Paper)},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {597--603},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_35},
  doi          = {10.1007/978-3-319-94821-8\_35},
  timestamp    = {Mon, 13 Dec 2021 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/WimmerH18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/WimmerHN18,
  author       = {Simon Wimmer and
                  Shuwei Hu and
                  Tobias Nipkow},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Verified Memoization and Dynamic Programming},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {579--596},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_34},
  doi          = {10.1007/978-3-319-94821-8\_34},
  timestamp    = {Mon, 13 Dec 2021 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/WimmerHN18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/ZhaoOS18,
  author       = {Jinxu Zhao and
                  Bruno C. d. S. Oliveira and
                  Tom Schrijvers},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Formalization of a Polymorphic Subtyping Algorithm},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {604--622},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_36},
  doi          = {10.1007/978-3-319-94821-8\_36},
  timestamp    = {Fri, 27 Mar 2020 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/itp/ZhaoOS18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/itp/ZmigrodDG18,
  author       = {Ran Zmigrod and
                  Matthew L. Daggitt and
                  Timothy G. Griffin},
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {An Agda Formalization of {\"{U}}resin and Dubois' Asynchronous
                  Fixed-Point Theory},
  booktitle    = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  pages        = {623--639},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8\_37},
  doi          = {10.1007/978-3-319-94821-8\_37},
  timestamp    = {Wed, 03 Oct 2018 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/ZmigrodDG18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/itp/2018,
  editor       = {Jeremy Avigad and
                  Assia Mahboubi},
  title        = {Interactive Theorem Proving - 9th International Conference, {ITP}
                  2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
                  UK, July 9-12, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10895},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-94821-8},
  doi          = {10.1007/978-3-319-94821-8},
  isbn         = {978-3-319-94820-1},
  timestamp    = {Tue, 14 May 2019 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/2018.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.