Search dblp for Publications

• > Home > Search

@inproceedings{DBLP:conf/aaai/Abdulaziz24,
  author       = {Mohammad Abdulaziz},
  editor       = {Michael J. Wooldridge and
                  Jennifer G. Dy and
                  Sriraam Natarajan},
  title        = {Interactive Theorem Provers: Applications in AI, Opportunities, and
                  Challenges},
  booktitle    = {Thirty-Eighth {AAAI} Conference on Artificial Intelligence, {AAAI}
                  2024, Thirty-Sixth Conference on Innovative Applications of Artificial
                  Intelligence, {IAAI} 2024, Fourteenth Symposium on Educational Advances
                  in Artificial Intelligence, {EAAI} 2014, February 20-27, 2024, Vancouver,
                  Canada},
  pages        = {22660},
  publisher    = {{AAAI} Press},
  year         = {2024},
  url          = {https://doi.org/10.1609/aaai.v38i20.30276},
  doi          = {10.1609/AAAI.V38I20.30276},
  timestamp    = {Tue, 02 Apr 2024 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/aaai/Abdulaziz24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/em/Kontorovich22,
  author       = {Alex Kontorovich},
  title        = {Foreword to: Special Issue on Interactive Theorem Provers},
  journal      = {Exp. Math.},
  volume       = {31},
  number       = {2},
  pages        = {347--348},
  year         = {2022},
  url          = {https://doi.org/10.1080/10586458.2022.2088982},
  doi          = {10.1080/10586458.2022.2088982},
  timestamp    = {Mon, 28 Aug 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/em/Kontorovich22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/corr/abs-2202-05207,
  author       = {Matthew L. Daggitt and
                  Wen Kokke and
                  Robert Atkey and
                  Luca Arnaboldi and
                  Ekaterina Komendantskaya},
  title        = {Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem
                  Provers},
  journal      = {CoRR},
  volume       = {abs/2202.05207},
  year         = {2022},
  url          = {https://arxiv.org/abs/2202.05207},
  eprinttype    = {arXiv},
  eprint       = {2202.05207},
  timestamp    = {Fri, 12 May 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2202-05207.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/fc/Hirai17,
  author       = {Yoichi Hirai},
  editor       = {Michael Brenner and
                  Kurt Rohloff and
                  Joseph Bonneau and
                  Andrew Miller and
                  Peter Y. A. Ryan and
                  Vanessa Teague and
                  Andrea Bracciali and
                  Massimiliano Sala and
                  Federico Pintore and
                  Markus Jakobsson},
  title        = {Defining the Ethereum Virtual Machine for Interactive Theorem Provers},
  booktitle    = {Financial Cryptography and Data Security - {FC} 2017 International
                  Workshops, WAHC, BITCOIN, VOTING, WTSC, and TA, Sliema, Malta, April
                  7, 2017, Revised Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {10323},
  pages        = {520--535},
  publisher    = {Springer},
  year         = {2017},
  url          = {https://doi.org/10.1007/978-3-319-70278-0\_33},
  doi          = {10.1007/978-3-319-70278-0\_33},
  timestamp    = {Tue, 16 Aug 2022 23:04:23 +0200},
  biburl       = {https://dblp.org/rec/conf/fc/Hirai17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/mscs/BoveKS16,
  author       = {Ana Bove and
                  Alexander Krauss and
                  Matthieu Sozeau},
  title        = {Partiality and recursion in interactive theorem provers - an overview},
  journal      = {Math. Struct. Comput. Sci.},
  volume       = {26},
  number       = {1},
  pages        = {38--88},
  year         = {2016},
  url          = {https://doi.org/10.1017/S0960129514000115},
  doi          = {10.1017/S0960129514000115},
  timestamp    = {Mon, 26 Feb 2024 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/journals/mscs/BoveKS16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cpp/Czajka16,
  author       = {Lukasz Czajka},
  editor       = {Jeremy Avigad and
                  Adam Chlipala},
  title        = {Improving automation in interactive theorem provers by efficient encoding
                  of lambda-abstractions},
  booktitle    = {Proceedings of the 5th {ACM} {SIGPLAN} Conference on Certified Programs
                  and Proofs, Saint Petersburg, FL, USA, January 20-22, 2016},
  pages        = {49--57},
  publisher    = {{ACM}},
  year         = {2016},
  url          = {https://doi.org/10.1145/2854065.2854069},
  doi          = {10.1145/2854065.2854069},
  timestamp    = {Tue, 06 Nov 2018 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/cpp/Czajka16.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/sefm/BeckertGB14,
  author       = {Bernhard Beckert and
                  Sarah Grebing and
                  Florian B{\"{o}}hl},
  editor       = {Carlos Canal and
                  Akram Idani},
  title        = {A Usability Evaluation of Interactive Theorem Provers Using Focus
                  Groups},
  booktitle    = {Software Engineering and Formal Methods - {SEFM} 2014 Collocated Workshops:
                  HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS, Grenoble, France, September
                  1-2, 2014, Revised Selected Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {8938},
  pages        = {3--19},
  publisher    = {Springer},
  year         = {2014},
  url          = {https://doi.org/10.1007/978-3-319-15201-1\_1},
  doi          = {10.1007/978-3-319-15201-1\_1},
  timestamp    = {Mon, 26 Jun 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/sefm/BeckertGB14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:journals/corr/BeckertGB14,
  author       = {Bernhard Beckert and
                  Sarah Grebing and
                  Florian B{\"{o}}hl},
  editor       = {Christoph Benzm{\"{u}}ller and
                  Bruno Woltzenlogel Paleo},
  title        = {How to Put Usability into Focus: Using Focus Groups to Evaluate the
                  Usability of Interactive Theorem Provers},
  booktitle    = {Proceedings Eleventh Workshop on User Interfaces for Theorem Provers,
                  {UITP} 2014, Vienna, Austria, 17th July 2014},
  series       = {{EPTCS}},
  volume       = {167},
  pages        = {4--13},
  year         = {2014},
  url          = {https://doi.org/10.4204/EPTCS.167.3},
  doi          = {10.4204/EPTCS.167.3},
  timestamp    = {Mon, 26 Jun 2023 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/BeckertGB14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/itp/2010par,
  editor       = {Ekaterina Komendantskaya and
                  Ana Bove and
                  Milad Niqui},
  title        = {Partiality and Recursion in Interactive Theorem Provers, PAR@ITP 2010,
                  Edinburgh, UK, July 15, 2010},
  series       = {EPiC Series},
  volume       = {5},
  publisher    = {EasyChair},
  year         = {2012},
  url          = {https://easychair.org/publications/volume/PAR-10},
  timestamp    = {Fri, 13 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/itp/2010par.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/Paulson10,
  author       = {Lawrence C. Paulson},
  editor       = {Renate A. Schmidt and
                  Stephan Schulz and
                  Boris Konev},
  title        = {Three Years of Experience with Sledgehammer, a Practical Link between
                  Automatic and Interactive Theorem Provers},
  booktitle    = {Proceedings of the 2nd Workshop on Practical Aspects of Automated
                  Reasoning, PAAR-2010, Edinburgh, Scotland, UK, July 14, 2010},
  series       = {EPiC Series in Computing},
  volume       = {9},
  pages        = {1--10},
  publisher    = {EasyChair},
  year         = {2010},
  url          = {https://doi.org/10.29007/tnfd},
  doi          = {10.29007/TNFD},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/Paulson10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/lpar/PaulsonB10,
  author       = {Lawrence C. Paulson and
                  Jasmin Christian Blanchette},
  editor       = {Geoff Sutcliffe and
                  Stephan Schulz and
                  Eugenia Ternovska},
  title        = {Three years of experience with Sledgehammer, a Practical Link Between
                  Automatic and Interactive Theorem Provers},
  booktitle    = {The 8th International Workshop on the Implementation of Logics, {IWIL}
                  2010, Yogyakarta, Indonesia, October 9, 2011},
  series       = {EPiC Series in Computing},
  volume       = {2},
  pages        = {1--11},
  publisher    = {EasyChair},
  year         = {2010},
  url          = {https://doi.org/10.29007/36dt},
  doi          = {10.29007/36DT},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/lpar/PaulsonB10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:journals/corr/abs-1012-4555,
  editor       = {Ana Bove and
                  Ekaterina Komendantskaya and
                  Milad Niqui},
  title        = {Proceedings Workshop on Partiality and Recursion in Interactive Theorem
                  Provers, {PAR} 2010, Edinburgh, UK, 15th July 2010},
  series       = {{EPTCS}},
  volume       = {43},
  year         = {2010},
  url          = {https://doi.org/10.4204/EPTCS.43},
  doi          = {10.4204/EPTCS.43},
  timestamp    = {Thu, 14 Oct 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-1012-4555.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@phdthesis{DBLP:phd/basesearch/Tassi08,
  author       = {Enrico Tassi},
  title        = {Interactive theorem provers: issues faced as a user and tackled as
                  a developer},
  school       = {University of Bologna, Italy},
  year         = {2008},
  url          = {http://amsdottorato.unibo.it/917/},
  timestamp    = {Fri, 19 May 2017 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/phd/basesearch/Tassi08.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/acsd/Schneider01,
  author       = {Klaus Schneider},
  title        = {Embedding Imperative Synchronous Languages in Interactive Theorem
                  Provers},
  booktitle    = {2nd International Conference on Application of Concurrency to System
                  Design {(ACSD} 2001), 25-30 June 2001, Newcastle upon Tyne, {UK}},
  pages        = {143},
  publisher    = {{IEEE} Computer Society},
  year         = {2001},
  url          = {https://doi.org/10.1109/CSD.2001.981772},
  doi          = {10.1109/CSD.2001.981772},
  timestamp    = {Fri, 24 Mar 2023 00:00:00 +0100},
  biburl       = {https://dblp.org/rec/conf/acsd/Schneider01.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tphol/HelkeK01,
  author       = {Steffen Helke and
                  Florian Kamm{\"{u}}ller},
  editor       = {Richard J. Boulton and
                  Paul B. Jackson},
  title        = {Representing Hierarchical Automata in Interactive Theorem Provers},
  booktitle    = {Theorem Proving in Higher Order Logics, 14th International Conference,
                  TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {2152},
  pages        = {233--248},
  publisher    = {Springer},
  year         = {2001},
  url          = {https://doi.org/10.1007/3-540-44755-5\_17},
  doi          = {10.1007/3-540-44755-5\_17},
  timestamp    = {Tue, 14 May 2019 10:00:48 +0200},
  biburl       = {https://dblp.org/rec/conf/tphol/HelkeK01.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/tphol/Moten98,
  author       = {Roderick Moten},
  editor       = {Jim Grundy and
                  Malcolm C. Newey},
  title        = {Exploiting Parallelism in Interactive Theorem Provers},
  booktitle    = {Theorem Proving in Higher Order Logics, 11th International Conference,
                  TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {1479},
  pages        = {315--330},
  publisher    = {Springer},
  year         = {1998},
  url          = {https://doi.org/10.1007/BFb0055144},
  doi          = {10.1007/BFB0055144},
  timestamp    = {Tue, 14 May 2019 10:00:48 +0200},
  biburl       = {https://dblp.org/rec/conf/tphol/Moten98.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/Suppes84,
  author       = {Patrick Suppes},
  editor       = {Robert E. Shostak},
  title        = {The Next Generation of Interactive Theorem Provers},
  booktitle    = {7th International Conference on Automated Deduction, Napa, California,
                  USA, May 14-16, 1984, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {170},
  pages        = {303--315},
  publisher    = {Springer},
  year         = {1984},
  url          = {https://doi.org/10.1007/978-0-387-34768-4\_18},
  doi          = {10.1007/978-0-387-34768-4\_18},
  timestamp    = {Tue, 14 May 2019 10:00:39 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/Suppes84.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}