Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDBibTeX records: Jasmin Blanchette
@article{DBLP:journals/afp/BlanchetteQT23,
author = {Jasmin Christian Blanchette and
Qi Qiu and
Sophie Tourret},
title = {Given Clause Loops},
journal = {Arch. Formal Proofs},
volume = {2023},
year = {2023},
url = {https://www.isa-afp.org/entries/Given\_Clause\_Loops.html},
timestamp = {Tue, 18 Apr 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/BlanchetteQT23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/cacm/BentkampBNTVW23,
author = {Alexander Bentkamp and
Jasmin Blanchette and
Visa Nummelin and
Sophie Tourret and
Petar Vukmirovic and
Uwe Waldmann},
title = {Mechanical Mathematicians},
journal = {Commun. {ACM}},
volume = {66},
number = {4},
pages = {80--90},
year = {2023},
url = {https://doi.org/10.1145/3557998},
doi = {10.1145/3557998},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/cacm/BentkampBNTVW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BentkampBTV23,
author = {Alexander Bentkamp and
Jasmin Blanchette and
Sophie Tourret and
Petar Vukmirovic},
title = {Superposition for Higher-Order Logic},
journal = {J. Autom. Reason.},
volume = {67},
number = {1},
pages = {10},
year = {2023},
url = {https://doi.org/10.1007/s10817-022-09649-9},
doi = {10.1007/S10817-022-09649-9},
timestamp = {Fri, 10 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jar/BentkampBTV23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/EbnerBT23,
author = {Gabriel Ebner and
Jasmin Blanchette and
Sophie Tourret},
title = {Unifying Splitting},
journal = {J. Autom. Reason.},
volume = {67},
number = {2},
pages = {16},
year = {2023},
url = {https://doi.org/10.1007/s10817-023-09660-8},
doi = {10.1007/S10817-023-09660-8},
timestamp = {Tue, 12 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/EbnerBT23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/lmcs/BlanchetteV23,
author = {Jasmin Blanchette and
Petar Vukmirovic},
title = {SAT-Inspired Higher-Order Eliminations},
journal = {Log. Methods Comput. Sci.},
volume = {19},
number = {2},
year = {2023},
url = {https://doi.org/10.46298/lmcs-19(2:9)2023},
doi = {10.46298/LMCS-19(2:9)2023},
timestamp = {Wed, 21 Jun 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/lmcs/BlanchetteV23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/siglog/BentkampBNTW23,
author = {Alexander Bentkamp and
Jasmin Blanchette and
Visa Nummelin and
Sophie Tourret and
Uwe Waldmann},
title = {Complete and Efficient Higher-Order Reasoning via Lambda-Superposition},
journal = {{ACM} {SIGLOG} News},
volume = {10},
number = {4},
pages = {25--40},
year = {2023},
url = {https://doi.org/10.1145/3636362.3636367},
doi = {10.1145/3636362.3636367},
timestamp = {Tue, 02 Jan 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/siglog/BentkampBNTW23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/tocl/VukmirovicBH23,
author = {Petar Vukmirovic and
Jasmin Blanchette and
Marijn J. H. Heule},
title = {SAT-Inspired Eliminations for Superposition},
journal = {{ACM} Trans. Comput. Log.},
volume = {24},
number = {1},
pages = {7:1--7:25},
year = {2023},
url = {https://doi.org/10.1145/3565366},
doi = {10.1145/3565366},
timestamp = {Sun, 16 Apr 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/tocl/VukmirovicBH23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BlanchetteQT23,
author = {Jasmin Blanchette and
Qi Qiu and
Sophie Tourret},
editor = {Brigitte Pientka and
Cesare Tinelli},
title = {Verified Given Clause Procedures},
booktitle = {Automated Deduction - {CADE} 29 - 29th International Conference on
Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14132},
pages = {61--77},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-38499-8\_4},
doi = {10.1007/978-3-031-38499-8\_4},
timestamp = {Thu, 14 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BlanchetteQT23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/NummelinBD23,
author = {Visa Nummelin and
Jasmin Blanchette and
Sander R. Dahmen},
editor = {Uli Sattler and
Martin Suda},
title = {Recurrence-Driven Summations in Automated Deduction},
booktitle = {Frontiers of Combining Systems - 14th International Symposium, FroCoS
2023, Prague, Czech Republic, September 20-22, 2023, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {14279},
pages = {23--40},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-43369-6\_2},
doi = {10.1007/978-3-031-43369-6\_2},
timestamp = {Wed, 01 Nov 2023 08:59:02 +0100},
biburl = {https://dblp.org/rec/conf/frocos/NummelinBD23.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 16:07:09 +0200},
biburl = {https://dblp.org/rec/conf/itp/DvorakB23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/VukmirovicBS23,
author = {Petar Vukmirovic and
Jasmin Blanchette and
Stephan Schulz},
editor = {Sriram Sankaranarayanan and
Natasha Sharygina},
title = {Extending a High-Performance Prover to Higher-Order Logic},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 29th International Conference, {TACAS} 2023, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2022, Paris, France, April 22-27, 2023, Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
volume = {13994},
pages = {111--129},
publisher = {Springer},
year = {2023},
url = {https://doi.org/10.1007/978-3-031-30820-8\_10},
doi = {10.1007/978-3-031-30820-8\_10},
timestamp = {Sat, 13 May 2023 01:07:18 +0200},
biburl = {https://dblp.org/rec/conf/tacas/VukmirovicBS23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/mkm/2021w,
editor = {Jasmin Blanchette and
James H. Davenport and
Peter Koepke and
Michael Kohlhase and
Andrea Kohlhase and
Adam Naumowicz and
Dennis M{\"{u}}ller and
Yasmine Sharoda and
Claudio Sacerdoti Coen},
title = {Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops,
Doctoral Program, and Work in Progress at the Conference on Intelligent
Computer Mathematics 2021 co-located with the 14th Conference on Intelligent
Computer Mathematics {(CICM} 2021), Virtual Event, Timisoara, Romania,
July 26 - 31, 2021},
series = {{CEUR} Workshop Proceedings},
volume = {3377},
publisher = {CEUR-WS.org},
year = {2023},
url = {https://ceur-ws.org/Vol-3377},
urn = {urn:nbn:de:0074-3377-5},
timestamp = {Thu, 14 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/mkm/2021w.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2302-06420,
author = {Martin Dvorak and
Jasmin Blanchette},
title = {Closure Properties of Unrestricted Grammars - Formally Verified},
journal = {CoRR},
volume = {abs/2302.06420},
year = {2023},
url = {https://doi.org/10.48550/arXiv.2302.06420},
doi = {10.48550/ARXIV.2302.06420},
eprinttype = {arXiv},
eprint = {2302.06420},
timestamp = {Mon, 20 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2302-06420.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/WaldmannTRB22,
author = {Uwe Waldmann and
Sophie Tourret and
Simon Robillard and
Jasmin Blanchette},
title = {A Comprehensive Framework for Saturation Theorem Proving},
journal = {J. Autom. Reason.},
volume = {66},
number = {4},
pages = {499--539},
year = {2022},
url = {https://doi.org/10.1007/s10817-022-09621-7},
doi = {10.1007/S10817-022-09621-7},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/WaldmannTRB22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/VukmirovicBBCNT22,
author = {Petar Vukmirovic and
Alexander Bentkamp and
Jasmin Blanchette and
Simon Cruanes and
Visa Nummelin and
Sophie Tourret},
title = {Making Higher-Order Superposition Work},
journal = {J. Autom. Reason.},
volume = {66},
number = {4},
pages = {541--564},
year = {2022},
url = {https://doi.org/10.1007/s10817-021-09613-z},
doi = {10.1007/S10817-021-09613-Z},
timestamp = {Mon, 05 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jar/VukmirovicBBCNT22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sttt/VukmirovicBCS22,
author = {Petar Vukmirovic and
Jasmin Blanchette and
Simon Cruanes and
Stephan Schulz},
title = {Extending a brainiac prover to lambda-free higher-order logic},
journal = {Int. J. Softw. Tools Technol. Transf.},
volume = {24},
number = {1},
pages = {67--87},
year = {2022},
url = {https://doi.org/10.1007/s10009-021-00639-7},
doi = {10.1007/S10009-021-00639-7},
timestamp = {Fri, 13 May 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/sttt/VukmirovicBCS22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/DesharnaisVBW22,
author = {Martin Desharnais and
Petar Vukmirovic and
Jasmin Blanchette and
Makarius Wenzel},
editor = {June Andronick and
Leonardo de Moura},
title = {Seventeen Provers Under the Hammer},
booktitle = {13th International Conference on Interactive Theorem Proving, {ITP}
2022, August 7-10, 2022, Haifa, Israel},
series = {LIPIcs},
volume = {237},
pages = {8:1--8:18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2022},
url = {https://doi.org/10.4230/LIPIcs.ITP.2022.8},
doi = {10.4230/LIPICS.ITP.2022.8},
timestamp = {Wed, 07 Dec 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/itp/DesharnaisVBW22.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2022,
editor = {Jasmin Blanchette and
Laura Kov{\'{a}}cs and
Dirk Pattinson},
title = {Automated Reasoning - 11th International Joint Conference, {IJCAR}
2022, Haifa, Israel, August 8-10, 2022, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {13385},
publisher = {Springer},
year = {2022},
url = {https://doi.org/10.1007/978-3-031-10769-6},
doi = {10.1007/978-3-031-10769-6},
isbn = {978-3-031-10768-9},
timestamp = {Mon, 24 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/2022.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2208-07775,
author = {Jasmin Blanchette and
Petar Vukmirovic},
title = {SAT-Inspired Higher-Order Eliminations},
journal = {CoRR},
volume = {abs/2208.07775},
year = {2022},
url = {https://doi.org/10.48550/arXiv.2208.07775},
doi = {10.48550/ARXIV.2208.07775},
eprinttype = {arXiv},
eprint = {2208.07775},
timestamp = {Mon, 22 Aug 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2208-07775.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/Blanchette21,
author = {Jasmin Blanchette},
title = {Message from the New Editor-in-Chief},
journal = {J. Autom. Reason.},
volume = {65},
number = {2},
pages = {155},
year = {2021},
url = {https://doi.org/10.1007/s10817-021-09587-y},
doi = {10.1007/S10817-021-09587-Y},
timestamp = {Fri, 09 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/Blanchette21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BentkampBTVW21,
author = {Alexander Bentkamp and
Jasmin Blanchette and
Sophie Tourret and
Petar Vukmirovic and
Uwe Waldmann},
title = {Superposition with Lambdas},
journal = {J. Autom. Reason.},
volume = {65},
number = {7},
pages = {893--940},
year = {2021},
url = {https://doi.org/10.1007/s10817-021-09595-y},
doi = {10.1007/S10817-021-09595-Y},
timestamp = {Tue, 28 Feb 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jar/BentkampBTVW21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/lmcs/BentkampBCW21,
author = {Alexander Bentkamp and
Jasmin Blanchette and
Simon Cruanes and
Uwe Waldmann},
title = {Superposition for Lambda-Free Higher-Order Logic},
journal = {Log. Methods Comput. Sci.},
volume = {17},
number = {2},
year = {2021},
url = {https://lmcs.episciences.org/7349},
timestamp = {Tue, 20 Apr 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/lmcs/BentkampBCW21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/EbnerBT21,
author = {Gabriel Ebner and
Jasmin Blanchette and
Sophie Tourret},
editor = {Andr{\'{e}} Platzer and
Geoff Sutcliffe},
title = {A Unifying Splitting Framework},
booktitle = {Automated Deduction - {CADE} 28 - 28th International Conference on
Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12699},
pages = {344--360},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-79876-5\_20},
doi = {10.1007/978-3-030-79876-5\_20},
timestamp = {Thu, 29 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/EbnerBT21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BentkampBTV21,
author = {Alexander Bentkamp and
Jasmin Blanchette and
Sophie Tourret and
Petar Vukmirovic},
editor = {Andr{\'{e}} Platzer and
Geoff Sutcliffe},
title = {Superposition for Full Higher-order Logic},
booktitle = {Automated Deduction - {CADE} 28 - 28th International Conference on
Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12699},
pages = {396--412},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-79876-5\_23},
doi = {10.1007/978-3-030-79876-5\_23},
timestamp = {Thu, 29 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BentkampBTV21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/VukmirovicBBCNT21,
author = {Petar Vukmirovic and
Alexander Bentkamp and
Jasmin Blanchette and
Simon Cruanes and
Visa Nummelin and
Sophie Tourret},
editor = {Andr{\'{e}} Platzer and
Geoff Sutcliffe},
title = {Making Higher-Order Superposition Work},
booktitle = {Automated Deduction - {CADE} 28 - 28th International Conference on
Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12699},
pages = {415--432},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-79876-5\_24},
doi = {10.1007/978-3-030-79876-5\_24},
timestamp = {Thu, 29 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/VukmirovicBBCNT21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/TourretB21,
author = {Sophie Tourret and
Jasmin Blanchette},
editor = {Catalin Hritcu and
Andrei Popescu},
title = {A modular Isabelle framework for verifying saturation provers},
booktitle = {{CPP} '21: 10th {ACM} {SIGPLAN} International Conference on Certified
Programs and Proofs, Virtual Event, Denmark, January 17-19, 2021},
pages = {224--237},
publisher = {{ACM}},
year = {2021},
url = {https://doi.org/10.1145/3437992.3439912},
doi = {10.1145/3437992.3439912},
timestamp = {Sat, 08 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cpp/TourretB21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fmcad/VukmirovicBH21,
author = {Petar Vukmirovic and
Jasmin Blanchette and
Marijn J. H. Heule},
title = {SAT-Inspired Eliminations for Superposition},
booktitle = {Formal Methods in Computer Aided Design, {FMCAD} 2021, New Haven,
CT, USA, October 19-22, 2021},
pages = {231--240},
publisher = {{IEEE}},
year = {2021},
url = {https://doi.org/10.34727/2021/isbn.978-3-85448-046-4\_32},
doi = {10.34727/2021/ISBN.978-3-85448-046-4\_32},
timestamp = {Sat, 09 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fmcad/VukmirovicBH21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/BlanchetteN21,
author = {Jasmin Blanchette and
Adam Naumowicz},
editor = {Jasmin Blanchette and
James H. Davenport and
Peter Koepke and
Michael Kohlhase and
Andrea Kohlhase and
Adam Naumowicz and
Dennis M{\"{u}}ller and
Yasmine Sharoda and
Claudio Sacerdoti Coen},
title = {{FMM} Preface},
booktitle = {Joint Proceedings of the FMM, FVPS, MathUI,NatFoM, and OpenMath Workshops,
Doctoral Program, and Work in Progress at the Conference on Intelligent
Computer Mathematics 2021 co-located with the 14th Conference on Intelligent
Computer Mathematics {(CICM} 2021), Virtual Event, Timisoara, Romania,
July 26 - 31, 2021},
series = {{CEUR} Workshop Proceedings},
volume = {3377},
publisher = {CEUR-WS.org},
year = {2021},
url = {https://ceur-ws.org/Vol-3377/fmm-preface.pdf},
timestamp = {Thu, 14 Sep 2023 09:27:13 +0200},
biburl = {https://dblp.org/rec/conf/mkm/BlanchetteN21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2102-00453,
author = {Alexander Bentkamp and
Jasmin Blanchette and
Sophie Tourret and
Petar Vukmirovic and
Uwe Waldmann},
title = {Superposition with Lambdas},
journal = {CoRR},
volume = {abs/2102.00453},
year = {2021},
url = {https://arxiv.org/abs/2102.00453},
eprinttype = {arXiv},
eprint = {2102.00453},
timestamp = {Tue, 09 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/abs-2102-00453.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/BlanchetteT20,
author = {Jasmin Blanchette and
Sophie Tourret},
title = {Extensions to the Comprehensive Framework for Saturation Theorem Proving},
journal = {Arch. Formal Proofs},
volume = {2020},
year = {2020},
url = {https://www.isa-afp.org/entries/Saturation\_Framework\_Extensions.html},
timestamp = {Wed, 17 Mar 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/afp/BlanchetteT20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BarbosaBFF20,
author = {Haniel Barbosa and
Jasmin Christian Blanchette and
Mathias Fleury and
Pascal Fontaine},
title = {Scalable Fine-Grained Proofs for Formula Processing},
journal = {J. Autom. Reason.},
volume = {64},
number = {3},
pages = {485--510},
year = {2020},
url = {https://doi.org/10.1007/s10817-018-09502-y},
doi = {10.1007/S10817-018-09502-Y},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BarbosaBFF20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/SchlichtkrullBT20,
author = {Anders Schlichtkrull and
Jasmin Blanchette and
Dmitriy Traytel and
Uwe Waldmann},
title = {Formalizing Bachmair and Ganzinger's Ordered Resolution Prover},
journal = {J. Autom. Reason.},
volume = {64},
number = {7},
pages = {1169--1195},
year = {2020},
url = {https://doi.org/10.1007/s10817-020-09561-0},
doi = {10.1007/S10817-020-09561-0},
timestamp = {Tue, 06 Oct 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/SchlichtkrullBT20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/WaldmannTRB20,
author = {Uwe Waldmann and
Sophie Tourret and
Simon Robillard and
Jasmin Blanchette},
editor = {Nicolas Peltier and
Viorica Sofronie{-}Stokkermans},
title = {A Comprehensive Framework for Saturation Theorem Proving},
booktitle = {Automated Reasoning - 10th International Joint Conference, {IJCAR}
2020, Paris, France, July 1-4, 2020, Proceedings, Part {I}},
series = {Lecture Notes in Computer Science},
volume = {12166},
pages = {316--334},
publisher = {Springer},
year = {2020},
url = {https://doi.org/10.1007/978-3-030-51074-9\_18},
doi = {10.1007/978-3-030-51074-9\_18},
timestamp = {Thu, 06 Aug 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/WaldmannTRB20.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cpp/2020,
editor = {Jasmin Blanchette and
Catalin Hritcu},
title = {Proceedings of the 9th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2020, New Orleans, LA, USA, January
20-21, 2020},
publisher = {{ACM}},
year = {2020},
url = {https://doi.org/10.1145/3372885},
doi = {10.1145/3372885},
isbn = {978-1-4503-7097-4},
timestamp = {Sun, 02 Oct 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/2020.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2005-02094,
author = {Alexander Bentkamp and
Jasmin Blanchette and
Simon Cruanes and
Uwe Waldmann},
title = {Superposition for Lambda-Free Higher-Order Logic},
journal = {CoRR},
volume = {abs/2005.02094},
year = {2020},
url = {https://arxiv.org/abs/2005.02094},
eprinttype = {arXiv},
eprint = {2005.02094},
timestamp = {Fri, 08 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2005-02094.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BlanchetteM19,
author = {Jasmin Christian Blanchette and
Stephan Merz},
title = {Selected Extended Papers of {ITP} 2016: Preface},
journal = {J. Autom. Reason.},
volume = {62},
number = {2},
pages = {169--170},
year = {2019},
url = {https://doi.org/10.1007/s10817-018-9470-8},
doi = {10.1007/S10817-018-9470-8},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BlanchetteM19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BentkampBK19,
author = {Alexander Bentkamp and
Jasmin Christian Blanchette and
Dietrich Klakow},
title = {A Formal Proof of the Expressiveness of Deep Learning},
journal = {J. Autom. Reason.},
volume = {63},
number = {2},
pages = {347--368},
year = {2019},
url = {https://doi.org/10.1007/s10817-018-9481-5},
doi = {10.1007/S10817-018-9481-5},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BentkampBK19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/pacmpl/BlanchetteGPT19,
author = {Jasmin Christian Blanchette and
Lorenzo Gheri and
Andrei Popescu and
Dmitriy Traytel},
title = {Bindings as bounded natural functors},
journal = {Proc. {ACM} Program. Lang.},
volume = {3},
number = {{POPL}},
pages = {22:1--22:34},
year = {2019},
url = {https://doi.org/10.1145/3290335},
doi = {10.1145/3290335},
timestamp = {Sat, 30 Sep 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/pacmpl/BlanchetteGPT19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sosym/BlanchetteBPKTW19,
author = {Jasmin Blanchette and
Francis Bordeleau and
Alfonso Pierantonio and
Nikolai Kosmatov and
Gabriele Taentzer and
Manuel Wimmer},
title = {Introduction to the {STAF} 2015 special section},
journal = {Softw. Syst. Model.},
volume = {18},
number = {1},
pages = {191--193},
year = {2019},
url = {https://doi.org/10.1007/s10270-018-0686-1},
doi = {10.1007/S10270-018-0686-1},
timestamp = {Fri, 18 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/sosym/BlanchetteBPKTW19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BentkampBTVW19,
author = {Alexander Bentkamp and
Jasmin Blanchette and
Sophie Tourret and
Petar Vukmirovic and
Uwe Waldmann},
editor = {Pascal Fontaine},
title = {Superposition with Lambdas},
booktitle = {Automated Deduction - {CADE} 27 - 27th International Conference on
Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {11716},
pages = {55--73},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-29436-6\_4},
doi = {10.1007/978-3-030-29436-6\_4},
timestamp = {Fri, 27 Mar 2020 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cade/BentkampBTVW19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/Blanchette19,
author = {Jasmin Christian Blanchette},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {Formalizing the metatheory of logical calculi and automatic provers
in Isabelle/HOL (invited talk)},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {1--13},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294087},
doi = {10.1145/3293880.3294087},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/Blanchette19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/SchlichtkrullBT19,
author = {Anders Schlichtkrull and
Jasmin Christian Blanchette and
Dmitriy Traytel},
editor = {Assia Mahboubi and
Magnus O. Myreen},
title = {A verified prover based on ordered resolution},
booktitle = {Proceedings of the 8th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2019, Cascais, Portugal, January
14-15, 2019},
pages = {152--165},
publisher = {{ACM}},
year = {2019},
url = {https://doi.org/10.1145/3293880.3294100},
doi = {10.1145/3293880.3294100},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/SchlichtkrullBT19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/VukmirovicBCS19,
author = {Petar Vukmirovic and
Jasmin Christian Blanchette and
Simon Cruanes and
Stephan Schulz},
editor = {Tom{\'{a}}s Vojnar and
Lijun Zhang},
title = {Extending a Brainiac Prover to Lambda-Free Higher-Order Logic},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 25th International Conference, {TACAS} 2019, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part
{I}},
series = {Lecture Notes in Computer Science},
volume = {11427},
pages = {192--210},
publisher = {Springer},
year = {2019},
url = {https://doi.org/10.1007/978-3-030-17462-0\_11},
doi = {10.1007/978-3-030-17462-0\_11},
timestamp = {Fri, 31 Jan 2020 21:32:25 +0100},
biburl = {https://dblp.org/rec/conf/tacas/VukmirovicBCS19.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/SchlichtkrullBT18,
author = {Anders Schlichtkrull and
Jasmin Christian Blanchette and
Dmitriy Traytel and
Uwe Waldmann},
title = {Formalization of Bachmair and Ganzinger's Ordered Resolution Prover},
journal = {Arch. Formal Proofs},
volume = {2018},
year = {2018},
url = {https://www.isa-afp.org/entries/Ordered\_Resolution\_Prover.html},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/SchlichtkrullBT18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/SchlichtkrullBT18a,
author = {Anders Schlichtkrull and
Jasmin Christian Blanchette and
Dmitriy Traytel},
title = {A Verified Functional Implementation of Bachmair and Ganzinger's Ordered
Resolution Prover},
journal = {Arch. Formal Proofs},
volume = {2018},
year = {2018},
url = {https://www.isa-afp.org/entries/Functional\_Ordered\_Resolution\_Prover.html},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/SchlichtkrullBT18a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/AvigadBKPPS18,
author = {Jeremy Avigad and
Jasmin Christian Blanchette and
Gerwin Klein and
Lawrence C. Paulson and
Andrei Popescu and
Gregor Snelting},
title = {Introduction to Milestones in Interactive Theorem Proving},
journal = {J. Autom. Reason.},
volume = {61},
number = {1-4},
pages = {1--8},
year = {2018},
url = {https://doi.org/10.1007/s10817-018-9465-5},
doi = {10.1007/S10817-018-9465-5},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/AvigadBKPPS18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BlanchetteFLW18,
author = {Jasmin Christian Blanchette and
Mathias Fleury and
Peter Lammich and
Christoph Weidenbach},
title = {A Verified {SAT} Solver Framework with Learn, Forget, Restart, and
Incrementality},
journal = {J. Autom. Reason.},
volume = {61},
number = {1-4},
pages = {333--365},
year = {2018},
url = {https://doi.org/10.1007/s10817-018-9455-7},
doi = {10.1007/S10817-018-9455-7},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BlanchetteFLW18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BentkampBCW18,
author = {Alexander Bentkamp and
Jasmin Christian Blanchette and
Simon Cruanes and
Uwe Waldmann},
editor = {Didier Galmiche and
Stephan Schulz and
Roberto Sebastiani},
title = {Superposition for Lambda-Free Higher-Order Logic},
booktitle = {Automated Reasoning - 9th International Joint Conference, {IJCAR}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 14-17, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10900},
pages = {28--46},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94205-6\_3},
doi = {10.1007/978-3-319-94205-6\_3},
timestamp = {Mon, 28 Aug 2023 21:17:45 +0200},
biburl = {https://dblp.org/rec/conf/cade/BentkampBCW18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/SchlichtkrullBT18,
author = {Anders Schlichtkrull and
Jasmin Christian Blanchette and
Dmitriy Traytel and
Uwe Waldmann},
editor = {Didier Galmiche and
Stephan Schulz and
Roberto Sebastiani},
title = {Formalizing Bachmair and Ganzinger's Ordered Resolution Prover},
booktitle = {Automated Reasoning - 9th International Joint Conference, {IJCAR}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 14-17, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10900},
pages = {89--107},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94205-6\_7},
doi = {10.1007/978-3-319-94205-6\_7},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/SchlichtkrullBT18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BlanchettePR18,
author = {Jasmin Christian Blanchette and
Nicolas Peltier and
Simon Robillard},
editor = {Didier Galmiche and
Stephan Schulz and
Roberto Sebastiani},
title = {Superposition with Datatypes and Codatatypes},
booktitle = {Automated Reasoning - 9th International Joint Conference, {IJCAR}
2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford,
UK, July 14-17, 2018, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10900},
pages = {370--387},
publisher = {Springer},
year = {2018},
url = {https://doi.org/10.1007/978-3-319-94205-6\_25},
doi = {10.1007/978-3-319-94205-6\_25},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BlanchettePR18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cpp/FleuryBL18,
author = {Mathias Fleury and
Jasmin Christian Blanchette and
Peter Lammich},
editor = {June Andronick and
Amy P. Felty},
title = {A verified {SAT} solver with watched literals using imperative {HOL}},
booktitle = {Proceedings of the 7th {ACM} {SIGPLAN} International Conference on
Certified Programs and Proofs, {CPP} 2018, Los Angeles, CA, USA, January
8-9, 2018},
pages = {158--171},
publisher = {{ACM}},
year = {2018},
url = {https://doi.org/10.1145/3167080},
doi = {10.1145/3167080},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cpp/FleuryBL18.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/BlanchettePT17,
author = {Jasmin Christian Blanchette and
Andrei Popescu and
Dmitriy Traytel},
title = {Abstract Soundness},
journal = {Arch. Formal Proofs},
volume = {2017},
year = {2017},
url = {https://www.isa-afp.org/entries/Abstract\_Soundness.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/BlanchettePT17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/BlanchettePT17a,
author = {Jasmin Christian Blanchette and
Andrei Popescu and
Dmitriy Traytel},
title = {Operations on Bounded Natural Functors},
journal = {Arch. Formal Proofs},
volume = {2017},
year = {2017},
url = {https://www.isa-afp.org/entries/BNF\_Operations.html},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/BlanchettePT17a.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BlanchettePT17,
author = {Jasmin Christian Blanchette and
Andrei Popescu and
Dmitriy Traytel},
title = {Soundness and Completeness Proofs by Coinductive Methods},
journal = {J. Autom. Reason.},
volume = {58},
number = {1},
pages = {149--179},
year = {2017},
url = {https://doi.org/10.1007/s10817-016-9391-3},
doi = {10.1007/S10817-016-9391-3},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BlanchettePT17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/ReynoldsB17,
author = {Andrew Reynolds and
Jasmin Christian Blanchette},
title = {A Decision Procedure for (Co)datatypes in {SMT} Solvers},
journal = {J. Autom. Reason.},
volume = {58},
number = {3},
pages = {341--362},
year = {2017},
url = {https://doi.org/10.1007/s10817-016-9372-6},
doi = {10.1007/S10817-016-9372-6},
timestamp = {Mon, 03 Jan 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jar/ReynoldsB17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BlanchetteF0W17,
author = {Jasmin Christian Blanchette and
Pascal Fontaine and
Stephan Schulz and
Uwe Waldmann},
editor = {Giles Reger and
Dmitriy Traytel},
title = {Towards Strong Higher-Order Automation for Fast Interactive Verification},
booktitle = {{ARCADE} 2017, 1st International Workshop on Automated Reasoning:
Challenges, Applications, Directions, Exemplary Achievements, Gothenburg,
Sweden, 6th August 2017},
series = {EPiC Series in Computing},
volume = {51},
pages = {16--23},
publisher = {EasyChair},
year = {2017},
url = {https://doi.org/10.29007/3ngx},
doi = {10.29007/3NGX},
timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BlanchetteF0W17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BarbosaBF17,
author = {Haniel Barbosa and
Jasmin Christian Blanchette and
Pascal Fontaine},
editor = {Leonardo de Moura},
title = {Scalable Fine-Grained Proofs for Formula Processing},
booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on
Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10395},
pages = {398--412},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-63046-5\_25},
doi = {10.1007/978-3-319-63046-5\_25},
timestamp = {Thu, 29 Sep 2022 08:36:56 +0200},
biburl = {https://dblp.org/rec/conf/cade/BarbosaBF17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BeckerBWW17,
author = {Heiko Becker and
Jasmin Christian Blanchette and
Uwe Waldmann and
Daniel Wand},
editor = {Leonardo de Moura},
title = {A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms},
booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on
Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10395},
pages = {432--453},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-63046-5\_27},
doi = {10.1007/978-3-319-63046-5\_27},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/BeckerBWW17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/BlanchetteBL0T17,
author = {Jasmin Christian Blanchette and
Aymeric Bouzy and
Andreas Lochbihler and
Andrei Popescu and
Dmitriy Traytel},
editor = {Hongseok Yang},
title = {Friends with Benefits - Implementing Corecursion in Foundational Proof
Assistants},
booktitle = {Programming Languages and Systems - 26th European Symposium on Programming,
{ESOP} 2017, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29,
2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10201},
pages = {111--140},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-662-54434-1\_5},
doi = {10.1007/978-3-662-54434-1\_5},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/esop/BlanchetteBL0T17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/fossacs/BlanchetteWW17,
author = {Jasmin Christian Blanchette and
Uwe Waldmann and
Daniel Wand},
editor = {Javier Esparza and
Andrzej S. Murawski},
title = {A Lambda-Free Higher-Order Recursive Path Order},
booktitle = {Foundations of Software Science and Computation Structures - 20th
International Conference, {FOSSACS} 2017, Held as Part of the European
Joint Conferences on Theory and Practice of Software, {ETAPS} 2017,
Uppsala, Sweden, April 22-29, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10203},
pages = {461--479},
year = {2017},
url = {https://doi.org/10.1007/978-3-662-54458-7\_27},
doi = {10.1007/978-3-662-54458-7\_27},
timestamp = {Sat, 19 Oct 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/fossacs/BlanchetteWW17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/BiendarraBBDFHK17,
author = {Julian Biendarra and
Jasmin Christian Blanchette and
Aymeric Bouzy and
Martin Desharnais and
Mathias Fleury and
Johannes H{\"{o}}lzl and
Ondrej Kuncar and
Andreas Lochbihler and
Fabian Meier and
Lorenz Panny and
Andrei Popescu and
Christian Sternagel and
Ren{\'{e}} Thiemann and
Dmitriy Traytel},
editor = {Clare Dixon and
Marcelo Finger},
title = {Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic},
booktitle = {Frontiers of Combining Systems - 11th International Symposium, FroCoS
2017, Bras{\'{\i}}lia, Brazil, September 27-29, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10483},
pages = {3--21},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-66167-4\_1},
doi = {10.1007/978-3-319-66167-4\_1},
timestamp = {Mon, 28 Aug 2023 21:17:55 +0200},
biburl = {https://dblp.org/rec/conf/frocos/BiendarraBBDFHK17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ijcai/BlanchetteFW17,
author = {Jasmin Christian Blanchette and
Mathias Fleury and
Christoph Weidenbach},
editor = {Carles Sierra},
title = {A Verified {SAT} Solver Framework with Learn, Forget, Restart, and
Incrementality},
booktitle = {Proceedings of the Twenty-Sixth International Joint Conference on
Artificial Intelligence, {IJCAI} 2017, Melbourne, Australia, August
19-25, 2017},
pages = {4786--4790},
publisher = {ijcai.org},
year = {2017},
url = {https://doi.org/10.24963/ijcai.2017/667},
doi = {10.24963/IJCAI.2017/667},
timestamp = {Sat, 05 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ijcai/BlanchetteFW17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/BentkampBK17,
author = {Alexander Bentkamp and
Jasmin Christian Blanchette and
Dietrich Klakow},
editor = {Mauricio Ayala{-}Rinc{\'{o}}n and
C{\'{e}}sar A. Mu{\~{n}}oz},
title = {A Formal Proof of the Expressiveness of Deep Learning},
booktitle = {Interactive Theorem Proving - 8th International Conference, {ITP}
2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {10499},
pages = {46--64},
publisher = {Springer},
year = {2017},
url = {https://doi.org/10.1007/978-3-319-66107-0\_4},
doi = {10.1007/978-3-319-66107-0\_4},
timestamp = {Mon, 05 Feb 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/itp/BentkampBK17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/BlanchetteM0T17,
author = {Jasmin Christian Blanchette and
Fabian Meier and
Andrei Popescu and
Dmitriy Traytel},
title = {Foundational nonuniform (Co)datatypes for higher-order logic},
booktitle = {32nd Annual {ACM/IEEE} Symposium on Logic in Computer Science, {LICS}
2017, Reykjavik, Iceland, June 20-23, 2017},
pages = {1--12},
publisher = {{IEEE} Computer Society},
year = {2017},
url = {https://doi.org/10.1109/LICS.2017.8005071},
doi = {10.1109/LICS.2017.8005071},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/BlanchetteM0T17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/rta/BlanchetteFT17,
author = {Jasmin Christian Blanchette and
Mathias Fleury and
Dmitriy Traytel},
editor = {Dale Miller},
title = {Nested Multisets, Hereditary Multisets, and Syntactic Ordinals in
Isabelle/HOL},
booktitle = {2nd International Conference on Formal Structures for Computation
and Deduction, {FSCD} 2017, September 3-9, 2017, Oxford, {UK}},
series = {LIPIcs},
volume = {84},
pages = {11:1--11:18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
year = {2017},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2017.11},
doi = {10.4230/LIPICS.FSCD.2017.11},
timestamp = {Tue, 11 Feb 2020 15:52:14 +0100},
biburl = {https://dblp.org/rec/conf/rta/BlanchetteFT17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/abs-1712-01486,
author = {Haniel Barbosa and
Jasmin Christian Blanchette and
Simon Cruanes and
Daniel El Ouraoui and
Pascal Fontaine},
editor = {Catherine Dubois and
Bruno Woltzenlogel Paleo},
title = {Language and Proofs for Higher-Order {SMT} (Work in Progress)},
booktitle = {Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving,
PxTP 2017, Bras{\'{\i}}lia, Brazil, 23-24 September 2017},
series = {{EPTCS}},
volume = {262},
pages = {15--22},
year = {2017},
url = {https://doi.org/10.4204/EPTCS.262.3},
doi = {10.4204/EPTCS.262.3},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-1712-01486.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/dagstuhl-reports/BlanchetteFST17,
author = {Jasmin Christian Blanchette and
Carsten Fuhs and
Viorica Sofronie{-}Stokkermans and
Cesare Tinelli},
title = {Deduction Beyond First-Order Logic (Dagstuhl Seminar 17371)},
journal = {Dagstuhl Reports},
volume = {7},
number = {9},
pages = {26--46},
year = {2017},
url = {https://doi.org/10.4230/DagRep.7.9.26},
doi = {10.4230/DAGREP.7.9.26},
timestamp = {Mon, 12 Mar 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/dagstuhl-reports/BlanchetteFST17.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/BeckerBWW16,
author = {Heiko Becker and
Jasmin Christian Blanchette and
Uwe Waldmann and
Daniel Wand},
title = {Formalization of Knuth-Bendix Orders for Lambda-Free Higher-Order
Terms},
journal = {Arch. Formal Proofs},
volume = {2016},
year = {2016},
url = {https://www.isa-afp.org/entries/Lambda\_Free\_KBOs.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/BeckerBWW16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/BlanchetteFT16,
author = {Jasmin Christian Blanchette and
Mathias Fleury and
Dmitriy Traytel},
title = {Formalization of Nested Multisets, Hereditary Multisets, and Syntactic
Ordinals},
journal = {Arch. Formal Proofs},
volume = {2016},
year = {2016},
url = {https://www.isa-afp.org/entries/Nested\_Multisets\_Ordinals.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/BlanchetteFT16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/BlanchetteWW16,
author = {Jasmin Christian Blanchette and
Uwe Waldmann and
Daniel Wand},
title = {Formalization of Recursive Path Orders for Lambda-Free Higher-Order
Terms},
journal = {Arch. Formal Proofs},
volume = {2016},
year = {2016},
url = {https://www.isa-afp.org/entries/Lambda\_Free\_RPOs.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/BlanchetteWW16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/BlanchetteB0S16,
author = {Jasmin Christian Blanchette and
Sascha B{\"{o}}hme and
Andrei Popescu and
Nicholas Smallbone},
title = {Encoding Monomorphic and Polymorphic Types},
journal = {Log. Methods Comput. Sci.},
volume = {12},
number = {4},
year = {2016},
url = {https://doi.org/10.2168/LMCS-12(4:13)2016},
doi = {10.2168/LMCS-12(4:13)2016},
timestamp = {Thu, 25 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/BlanchetteB0S16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BlanchetteBFSS16,
author = {Jasmin Christian Blanchette and
Sascha B{\"{o}}hme and
Mathias Fleury and
Steffen Juilf Smolka and
Albert Steckermeier},
title = {Semi-intelligible Isar Proofs from Machine-Generated Proofs},
journal = {J. Autom. Reason.},
volume = {56},
number = {2},
pages = {155--200},
year = {2016},
url = {https://doi.org/10.1007/s10817-015-9335-3},
doi = {10.1007/S10817-015-9335-3},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BlanchetteBFSS16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BlanchetteGKKU16,
author = {Jasmin Christian Blanchette and
David Greenaway and
Cezary Kaliszyk and
Daniel K{\"{u}}hlwein and
Josef Urban},
title = {A Learning-Based Fact Selector for Isabelle/HOL},
journal = {J. Autom. Reason.},
volume = {57},
number = {3},
pages = {219--244},
year = {2016},
url = {https://doi.org/10.1007/s10817-016-9362-8},
doi = {10.1007/S10817-016-9362-8},
timestamp = {Wed, 16 Mar 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jar/BlanchetteGKKU16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jfrea/BlanchetteKPU16,
author = {Jasmin Christian Blanchette and
Cezary Kaliszyk and
Lawrence C. Paulson and
Josef Urban},
title = {Hammering towards {QED}},
journal = {J. Formaliz. Reason.},
volume = {9},
number = {1},
pages = {101--148},
year = {2016},
url = {https://doi.org/10.6092/issn.1972-5787/4593},
doi = {10.6092/ISSN.1972-5787/4593},
timestamp = {Thu, 24 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jfrea/BlanchetteKPU16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BlanchetteFW16,
author = {Jasmin Christian Blanchette and
Mathias Fleury and
Christoph Weidenbach},
editor = {Nicola Olivetti and
Ashish Tiwari},
title = {A Verified {SAT} Solver Framework with Learn, Forget, Restart, and
Incrementality},
booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9706},
pages = {25--44},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-40229-1\_4},
doi = {10.1007/978-3-319-40229-1\_4},
timestamp = {Mon, 26 Jun 2023 20:45:22 +0200},
biburl = {https://dblp.org/rec/conf/cade/BlanchetteFW16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/ReynoldsBCT16,
author = {Andrew Reynolds and
Jasmin Christian Blanchette and
Simon Cruanes and
Cesare Tinelli},
editor = {Nicola Olivetti and
Ashish Tiwari},
title = {Model Finding for Recursive Functions in {SMT}},
booktitle = {Automated Reasoning - 8th International Joint Conference, {IJCAR}
2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9706},
pages = {133--151},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-40229-1\_10},
doi = {10.1007/978-3-319-40229-1\_10},
timestamp = {Tue, 27 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/ReynoldsBCT16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ijcai/ReynoldsB16,
author = {Andrew Reynolds and
Jasmin Christian Blanchette},
editor = {Subbarao Kambhampati},
title = {A Decision Procedure for (Co)datatypes in {SMT} Solvers},
booktitle = {Proceedings of the Twenty-Fifth International Joint Conference on
Artificial Intelligence, {IJCAI} 2016, New York, NY, USA, 9-15 July
2016},
pages = {4205--4209},
publisher = {{IJCAI/AAAI} Press},
year = {2016},
url = {http://www.ijcai.org/Abstract/16/631},
timestamp = {Tue, 27 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/ijcai/ReynoldsB16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/corr/CruanesB16,
author = {Simon Cruanes and
Jasmin Christian Blanchette},
editor = {Jasmin Christian Blanchette and
Cezary Kaliszyk},
title = {Extending Nunchaku to Dependent Type Theory},
booktitle = {Proceedings First International Workshop on Hammers for Type Theories,
HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016},
series = {{EPTCS}},
volume = {210},
pages = {3--12},
year = {2016},
url = {https://doi.org/10.4204/EPTCS.210.3},
doi = {10.4204/EPTCS.210.3},
timestamp = {Wed, 16 Mar 2022 23:52:32 +0100},
biburl = {https://dblp.org/rec/journals/corr/CruanesB16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/itp/2016,
editor = {Jasmin Christian Blanchette and
Stephan Merz},
title = {Interactive Theorem Proving - 7th International Conference, {ITP}
2016, Nancy, France, August 22-25, 2016, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9807},
publisher = {Springer},
year = {2016},
url = {https://doi.org/10.1007/978-3-319-43144-4},
doi = {10.1007/978-3-319-43144-4},
isbn = {978-3-319-43143-7},
timestamp = {Tue, 14 May 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/2016.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:journals/corr/BlanchetteK16,
editor = {Jasmin Christian Blanchette and
Cezary Kaliszyk},
title = {Proceedings First International Workshop on Hammers for Type Theories,
HaTT@IJCAR 2016, Coimbra, Portugal, July 1, 2016},
series = {{EPTCS}},
volume = {210},
year = {2016},
url = {https://doi.org/10.4204/EPTCS.210},
doi = {10.4204/EPTCS.210},
timestamp = {Wed, 16 Mar 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/corr/BlanchetteK16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/ReynoldsB15,
author = {Andrew Reynolds and
Jasmin Christian Blanchette},
editor = {Amy P. Felty and
Aart Middeldorp},
title = {A Decision Procedure for (Co)datatypes in {SMT} Solvers},
booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on
Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9195},
pages = {197--213},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-21401-6\_13},
doi = {10.1007/978-3-319-21401-6\_13},
timestamp = {Tue, 27 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/ReynoldsB15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/esop/Blanchette0T15,
author = {Jasmin Christian Blanchette and
Andrei Popescu and
Dmitriy Traytel},
editor = {Jan Vitek},
title = {Witnessing (Co)datatypes},
booktitle = {Programming Languages and Systems - 24th European Symposium on Programming,
{ESOP} 2015, Held as Part of the European Joint Conferences on Theory
and Practice of Software, {ETAPS} 2015, London, UK, April 11-18, 2015.
Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9032},
pages = {359--382},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-662-46669-8\_15},
doi = {10.1007/978-3-662-46669-8\_15},
timestamp = {Tue, 20 Aug 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/esop/Blanchette0T15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/icfp/Blanchette0T15,
author = {Jasmin Christian Blanchette and
Andrei Popescu and
Dmitriy Traytel},
editor = {Kathleen Fisher and
John H. Reppy},
title = {Foundational extensible corecursion: a proof assistant perspective},
booktitle = {Proceedings of the 20th {ACM} {SIGPLAN} International Conference on
Functional Programming, {ICFP} 2015, Vancouver, BC, Canada, September
1-3, 2015},
pages = {192--204},
publisher = {{ACM}},
year = {2015},
url = {https://doi.org/10.1145/2784731.2784732},
doi = {10.1145/2784731.2784732},
timestamp = {Wed, 23 Jun 2021 16:58:51 +0200},
biburl = {https://dblp.org/rec/conf/icfp/Blanchette0T15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/mkm/BlanchetteHMN15,
author = {Jasmin Christian Blanchette and
Max W. Haslbeck and
Daniel Matichuk and
Tobias Nipkow},
editor = {Manfred Kerber and
Jacques Carette and
Cezary Kaliszyk and
Florian Rabe and
Volker Sorge},
title = {Mining the Archive of Formal Proofs},
booktitle = {Intelligent Computer Mathematics - International Conference, {CICM}
2015, Washington, DC, USA, July 13-17, 2015, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9150},
pages = {3--17},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-20615-8\_1},
doi = {10.1007/978-3-319-20615-8\_1},
timestamp = {Mon, 28 Aug 2023 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/mkm/BlanchetteHMN15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/tap/2015,
editor = {Jasmin Christian Blanchette and
Nikolai Kosmatov},
title = {Tests and Proofs - 9th International Conference, TAP@STAF 2015, L'Aquila,
Italy, July 22-24, 2015. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {9154},
publisher = {Springer},
year = {2015},
url = {https://doi.org/10.1007/978-3-319-21215-9},
doi = {10.1007/978-3-319-21215-9},
isbn = {978-3-319-21214-2},
timestamp = {Tue, 23 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/tap/2015.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/Blanchette0T15,
author = {Jasmin Christian Blanchette and
Andrei Popescu and
Dmitriy Traytel},
title = {Foundational Extensible Corecursion},
journal = {CoRR},
volume = {abs/1501.05425},
year = {2015},
url = {http://arxiv.org/abs/1501.05425},
eprinttype = {arXiv},
eprint = {1501.05425},
timestamp = {Mon, 13 Aug 2018 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/corr/Blanchette0T15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/dagstuhl-reports/BjornerBSW15,
author = {Nikolaj S. Bj{\o}rner and
Jasmin Christian Blanchette and
Viorica Sofronie{-}Stokkermans and
Christoph Weidenbach},
title = {Information from Deduction: Models and Proofs (Dagstuhl Seminar 15381)},
journal = {Dagstuhl Reports},
volume = {5},
number = {9},
pages = {18--37},
year = {2015},
url = {https://doi.org/10.4230/DagRep.5.9.18},
doi = {10.4230/DAGREP.5.9.18},
timestamp = {Thu, 14 Apr 2022 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/dagstuhl-reports/BjornerBSW15.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/Blanchette0T14,
author = {Jasmin Christian Blanchette and
Andrei Popescu and
Dmitriy Traytel},
title = {Abstract Completeness},
journal = {Arch. Formal Proofs},
volume = {2014},
year = {2014},
url = {https://www.isa-afp.org/entries/Abstract\_Completeness.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/Blanchette0T14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Blanchette14,
author = {Jasmin Christian Blanchette},
editor = {Laura Kov{\'{a}}cs and
Andrei Voronkov},
title = {My Life with an Automatic Theorem Prover},
booktitle = {Proceedings of the 1st and 2nd Vampire Workshops, Vampire@VSL 2014,
Vienna, Austria, July 23, 2014 / Vampire@CADE 2015, Berlin, Germany,
August 2, 2015},
series = {EPiC Series in Computing},
volume = {38},
pages = {1--7},
publisher = {EasyChair},
year = {2014},
url = {https://doi.org/10.29007/5b7w},
doi = {10.29007/5B7W},
timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/Blanchette14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Blanchette0T14,
author = {Jasmin Christian Blanchette and
Andrei Popescu and
Dmitriy Traytel},
editor = {St{\'{e}}phane Demri and
Deepak Kapur and
Christoph Weidenbach},
title = {Unified Classical Logic Completeness - {A} Coinductive Pearl},
booktitle = {Automated Reasoning - 7th International Joint Conference, {IJCAR}
2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
Austria, July 19-22, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8562},
pages = {46--60},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08587-6\_4},
doi = {10.1007/978-3-319-08587-6\_4},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/Blanchette0T14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/haskell/BlanchetteHNNT14,
author = {Jasmin Christian Blanchette and
Lars Hupel and
Tobias Nipkow and
Lars Noschinski and
Dmitriy Traytel},
editor = {Wouter Swierstra},
title = {Experience report: the next 1100 Haskell programmers},
booktitle = {Proceedings of the 2014 {ACM} {SIGPLAN} symposium on Haskell, Gothenburg,
Sweden, September 4-5, 2014},
pages = {25--30},
publisher = {{ACM}},
year = {2014},
url = {https://doi.org/10.1145/2633357.2633359},
doi = {10.1145/2633357.2633359},
timestamp = {Thu, 24 Jun 2021 16:19:29 +0200},
biburl = {https://dblp.org/rec/conf/haskell/BlanchetteHNNT14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/BlanchetteHLP0T14,
author = {Jasmin Christian Blanchette and
Johannes H{\"{o}}lzl and
Andreas Lochbihler and
Lorenz Panny and
Andrei Popescu and
Dmitriy Traytel},
editor = {Gerwin Klein and
Ruben Gamboa},
title = {Truly Modular (Co)datatypes for Isabelle/HOL},
booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP}
2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
Austria, July 14-17, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8558},
pages = {93--110},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08970-6\_7},
doi = {10.1007/978-3-319-08970-6\_7},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/BlanchetteHLP0T14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/Blanchette0T14,
author = {Jasmin Christian Blanchette and
Andrei Popescu and
Dmitriy Traytel},
editor = {Gerwin Klein and
Ruben Gamboa},
title = {Cardinals in Isabelle/HOL},
booktitle = {Interactive Theorem Proving - 5th International Conference, {ITP}
2014, Held as Part of the Vienna Summer of Logic, {VSL} 2014, Vienna,
Austria, July 14-17, 2014. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8558},
pages = {111--127},
publisher = {Springer},
year = {2014},
url = {https://doi.org/10.1007/978-3-319-08970-6\_8},
doi = {10.1007/978-3-319-08970-6\_8},
timestamp = {Fri, 02 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/itp/Blanchette0T14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/Blanchette013,
author = {Jasmin Christian Blanchette and
Andrei Popescu},
title = {Sound and Complete Sort Encodings for First-Order Logic},
journal = {Arch. Formal Proofs},
volume = {2013},
year = {2013},
url = {https://www.isa-afp.org/entries/Sort\_Encodings.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/Blanchette013.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/japll/SultanaBP13,
author = {Nik Sultana and
Jasmin Christian Blanchette and
Lawrence C. Paulson},
title = {{LEO-II} and Satallax on the Sledgehammer test bench},
journal = {J. Appl. Log.},
volume = {11},
number = {1},
pages = {91--102},
year = {2013},
url = {https://doi.org/10.1016/j.jal.2012.12.002},
doi = {10.1016/J.JAL.2012.12.002},
timestamp = {Tue, 16 Feb 2021 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/japll/SultanaBP13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BlanchetteBP13,
author = {Jasmin Christian Blanchette and
Sascha B{\"{o}}hme and
Lawrence C. Paulson},
title = {Extending Sledgehammer with {SMT} Solvers},
journal = {J. Autom. Reason.},
volume = {51},
number = {1},
pages = {109--128},
year = {2013},
url = {https://doi.org/10.1007/s10817-013-9278-5},
doi = {10.1007/S10817-013-9278-5},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/BlanchetteBP13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/sqj/Blanchette13,
author = {Jasmin Christian Blanchette},
title = {Relational analysis of (co)inductive predicates, (co)algebraic datatypes,
and (co)recursive functions},
journal = {Softw. Qual. J.},
volume = {21},
number = {1},
pages = {101--126},
year = {2013},
url = {https://doi.org/10.1007/s11219-011-9148-5},
doi = {10.1007/S11219-011-9148-5},
timestamp = {Mon, 08 Jun 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/sqj/Blanchette13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/Blanchette13,
author = {Jasmin Christian Blanchette},
editor = {Jasmin Christian Blanchette and
Josef Urban},
title = {Redirecting Proofs by Contradiction},
booktitle = {Third International Workshop on Proof Exchange for Theorem Proving,
PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
series = {EPiC Series in Computing},
volume = {14},
pages = {11--26},
publisher = {EasyChair},
year = {2013},
url = {https://doi.org/10.29007/wm8b},
doi = {10.29007/WM8B},
timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/Blanchette13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/SmolkaB13,
author = {Steffen Juilf Smolka and
Jasmin Christian Blanchette},
editor = {Jasmin Christian Blanchette and
Josef Urban},
title = {Robust, Semi-Intelligible Isabelle Proofs from {ATP} Proofs},
booktitle = {Third International Workshop on Proof Exchange for Theorem Proving,
PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
series = {EPiC Series in Computing},
volume = {14},
pages = {117--132},
publisher = {EasyChair},
year = {2013},
url = {https://doi.org/10.29007/zbdb},
doi = {10.29007/ZBDB},
timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/SmolkaB13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BlanchetteP13,
author = {Jasmin Christian Blanchette and
Andrei Paskevich},
editor = {Maria Paola Bonacina},
title = {{TFF1:} The {TPTP} Typed First-Order Form with Rank-1 Polymorphism},
booktitle = {Automated Deduction - {CADE-24} - 24th International Conference on
Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7898},
pages = {414--420},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-38574-2\_29},
doi = {10.1007/978-3-642-38574-2\_29},
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
biburl = {https://dblp.org/rec/conf/cade/BlanchetteP13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/Blanchette013,
author = {Jasmin Christian Blanchette and
Andrei Popescu},
editor = {Pascal Fontaine and
Christophe Ringeissen and
Renate A. Schmidt},
title = {Mechanizing the Metatheory of Sledgehammer},
booktitle = {Frontiers of Combining Systems - 9th International Symposium, FroCoS
2013, Nancy, France, September 18-20, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {8152},
pages = {245--260},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-40885-4\_17},
doi = {10.1007/978-3-642-40885-4\_17},
timestamp = {Tue, 14 May 2019 10:00:51 +0200},
biburl = {https://dblp.org/rec/conf/frocos/Blanchette013.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/KuhlweinBKU13,
author = {Daniel K{\"{u}}hlwein and
Jasmin Christian Blanchette and
Cezary Kaliszyk and
Josef Urban},
editor = {Sandrine Blazy and
Christine Paulin{-}Mohring and
David Pichardie},
title = {MaSh: Machine Learning for Sledgehammer},
booktitle = {Interactive Theorem Proving - 4th International Conference, {ITP}
2013, Rennes, France, July 22-26, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7998},
pages = {35--50},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-39634-2\_6},
doi = {10.1007/978-3-642-39634-2\_6},
timestamp = {Wed, 16 Mar 2022 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/itp/KuhlweinBKU13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tacas/BlanchetteBPS13,
author = {Jasmin Christian Blanchette and
Sascha B{\"{o}}hme and
Andrei Popescu and
Nicholas Smallbone},
editor = {Nir Piterman and
Scott A. Smolka},
title = {Encoding Monomorphic and Polymorphic Types},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
- 19th International Conference, {TACAS} 2013, Held as Part of the
European Joint Conferences on Theory and Practice of Software, {ETAPS}
2013, Rome, Italy, March 16-24, 2013. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7795},
pages = {493--507},
publisher = {Springer},
year = {2013},
url = {https://doi.org/10.1007/978-3-642-36742-7\_34},
doi = {10.1007/978-3-642-36742-7\_34},
timestamp = {Tue, 14 May 2019 10:00:53 +0200},
biburl = {https://dblp.org/rec/conf/tacas/BlanchetteBPS13.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@proceedings{DBLP:conf/cade/2013pxtp,
editor = {Jasmin Christian Blanchette and
Josef Urban},
title = {Third International Workshop on Proof Exchange for Theorem Proving,
PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
year = {2013},
url = {https://easychair.org/publications/volume/PxTP\_2013},
timestamp = {Fri, 13 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/cade/2013pxtp.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@phdthesis{DBLP:phd/dnb/Blanchette12,
author = {Jasmin Christian Blanchette},
title = {Automatic proofs and refutations for higher-order logic},
school = {Technical University Munich},
year = {2012},
url = {https://nbn-resolving.org/urn:nbn:de:bvb:91-diss-20120628-1097834-1-6},
urn = {urn:nbn:de:bvb:91-diss-20120628-1097834-1-6},
timestamp = {Sat, 17 Jul 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/phd/dnb/Blanchette12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/BlanchettePWW12,
author = {Jasmin Christian Blanchette and
Andrei Popescu and
Daniel Wand and
Christoph Weidenbach},
editor = {Lennart Beringer and
Amy P. Felty},
title = {More {SPASS} with Isabelle - Superposition with Hard Sorts and Configurable
Simplification},
booktitle = {Interactive Theorem Proving - Third International Conference, {ITP}
2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7406},
pages = {345--360},
publisher = {Springer},
year = {2012},
url = {https://doi.org/10.1007/978-3-642-32347-8\_24},
doi = {10.1007/978-3-642-32347-8\_24},
timestamp = {Tue, 14 May 2019 10:00:37 +0200},
biburl = {https://dblp.org/rec/conf/itp/BlanchettePWW12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lics/TraytelPB12,
author = {Dmitriy Traytel and
Andrei Popescu and
Jasmin Christian Blanchette},
title = {Foundational, Compositional (Co)datatypes for Higher-Order Logic:
Category Theory Applied to Theorem Proving},
booktitle = {Proceedings of the 27th Annual {IEEE} Symposium on Logic in Computer
Science, {LICS} 2012, Dubrovnik, Croatia, June 25-28, 2012},
pages = {596--605},
publisher = {{IEEE} Computer Society},
year = {2012},
url = {https://doi.org/10.1109/LICS.2012.75},
doi = {10.1109/LICS.2012.75},
timestamp = {Fri, 24 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/lics/TraytelPB12.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/BlanchetteK11,
author = {Jasmin Christian Blanchette and
Alexander Krauss},
title = {Monotonicity Inference for Higher-Order Formulas},
journal = {J. Autom. Reason.},
volume = {47},
number = {4},
pages = {369--398},
year = {2011},
url = {https://doi.org/10.1007/s10817-011-9234-1},
doi = {10.1007/S10817-011-9234-1},
timestamp = {Mon, 26 Feb 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/jar/BlanchetteK11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BlanchetteBP11,
author = {Jasmin Christian Blanchette and
Sascha B{\"{o}}hme and
Lawrence C. Paulson},
editor = {Nikolaj S. Bj{\o}rner and
Viorica Sofronie{-}Stokkermans},
title = {Extending Sledgehammer with {SMT} Solvers},
booktitle = {Automated Deduction - {CADE-23} - 23rd International Conference on
Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6803},
pages = {116--130},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-22438-6\_11},
doi = {10.1007/978-3-642-22438-6\_11},
timestamp = {Mon, 28 Aug 2023 21:17:45 +0200},
biburl = {https://dblp.org/rec/conf/cade/BlanchetteBP11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/frocos/BlanchetteBN11,
author = {Jasmin Christian Blanchette and
Lukas Bulwahn and
Tobias Nipkow},
editor = {Cesare Tinelli and
Viorica Sofronie{-}Stokkermans},
title = {Automatic Proof and Disproof in Isabelle/HOL},
booktitle = {Frontiers of Combining Systems, 8th International Symposium, FroCoS
2011, Saarbr{\"{u}}cken, Germany, October 5-7, 2011. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6989},
pages = {12--27},
publisher = {Springer},
year = {2011},
url = {https://doi.org/10.1007/978-3-642-24364-6\_2},
doi = {10.1007/978-3-642-24364-6\_2},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/frocos/BlanchetteBN11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/ppdp/BlanchetteWBOS11,
author = {Jasmin Christian Blanchette and
Tjark Weber and
Mark Batty and
Scott Owens and
Susmit Sarkar},
editor = {Peter Schneider{-}Kamp and
Michael Hanus},
title = {Nitpicking {C++} concurrency},
booktitle = {Proceedings of the 13th International {ACM} {SIGPLAN} Conference on
Principles and Practice of Declarative Programming, July 20-22, 2011,
Odense, Denmark},
pages = {113--124},
publisher = {{ACM}},
year = {2011},
url = {https://doi.org/10.1145/2003476.2003493},
doi = {10.1145/2003476.2003493},
timestamp = {Tue, 06 Nov 2018 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/ppdp/BlanchetteWBOS11.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/cade/BlanchetteK10,
author = {Jasmin Christian Blanchette and
Alexander Krauss},
editor = {J{\"{u}}rgen Giesl and
Reiner H{\"{a}}hnle},
title = {Monotonicity Inference for Higher-Order Formulas},
booktitle = {Automated Reasoning, 5th International Joint Conference, {IJCAR} 2010,
Edinburgh, UK, July 16-19, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6173},
pages = {91--106},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14203-1\_8},
doi = {10.1007/978-3-642-14203-1\_8},
timestamp = {Mon, 26 Feb 2024 00:00:00 +0100},
biburl = {https://dblp.org/rec/conf/cade/BlanchetteK10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/itp/BlanchetteN10,
author = {Jasmin Christian Blanchette and
Tobias Nipkow},
editor = {Matt Kaufmann and
Lawrence C. Paulson},
title = {Nitpick: {A} Counterexample Generator for Higher-Order Logic Based
on a Relational Model Finder},
booktitle = {Interactive Theorem Proving, First International Conference, {ITP}
2010, Edinburgh, UK, July 11-14, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6172},
pages = {131--146},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-14052-5\_11},
doi = {10.1007/978-3-642-14052-5\_11},
timestamp = {Wed, 25 Sep 2019 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/itp/BlanchetteN10.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}
}
@inproceedings{DBLP:conf/lpar/Blanchette10,
author = {Jasmin Christian Blanchette},
editor = {Andrei Voronkov and
Geoff Sutcliffe and
Matthias Baaz and
Christian G. Ferm{\"{u}}ller},
title = {Nitpick: {A} Counterexample Generator for Isabelle/HOL Based on the
Relational Model Finder Kodkod},
booktitle = {Short papers for 17th International Conference on Logic for Programming,
Artificial intelligence, and Reasoning, LPAR-17-short, Yogyakarta,
Indonesia, October 10-15, 2010},
series = {EPiC Series in Computing},
volume = {13},
pages = {20--25},
publisher = {EasyChair},
year = {2010},
url = {https://doi.org/10.29007/6shf},
doi = {10.29007/6SHF},
timestamp = {Sun, 15 Aug 2021 01:00:00 +0200},
biburl = {https://dblp.org/rec/conf/lpar/Blanchette10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/lpar/BlanchetteC10,
author = {Jasmin Christian Blanchette and
Koen Claessen},
editor = {Christian G. Ferm{\"{u}}ller and
Andrei Voronkov},
title = {Generating Counterexamples for Structural Inductions by Exploiting
Nonstandard Models},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning - 17th
International Conference, LPAR-17, Yogyakarta, Indonesia, October
10-15, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6397},
pages = {127--141},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-16242-8\_10},
doi = {10.1007/978-3-642-16242-8\_10},
timestamp = {Tue, 14 May 2019 10:00:55 +0200},
biburl = {https://dblp.org/rec/conf/lpar/BlanchetteC10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:conf/tap/Blanchette10,
author = {Jasmin Christian Blanchette},
editor = {Gordon Fraser and
Angelo Gargantini},
title = {Relational Analysis of (Co)inductive Predicates, (Co)algebraic Datatypes,
and (Co)recursive Functions},
booktitle = {Tests and Proofs - 4th International Conference, TAP@TOOLS 2010, M{\'{a}}laga,
Spain, July 1-2, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {6143},
pages = {117--134},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-13977-2\_11},
doi = {10.1007/978-3-642-13977-2\_11},
timestamp = {Mon, 23 Nov 2020 12:33:05 +0100},
biburl = {https://dblp.org/rec/conf/tap/Blanchette10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/jar/Blanchette09,
author = {Jasmin Christian Blanchette},
title = {Proof Pearl: Mechanizing the Textbook Proof of Huffman's Algorithm},
journal = {J. Autom. Reason.},
volume = {43},
number = {1},
pages = {1--18},
year = {2009},
url = {https://doi.org/10.1007/s10817-009-9116-y},
doi = {10.1007/S10817-009-9116-Y},
timestamp = {Wed, 02 Sep 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/jar/Blanchette09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{DBLP:books/daglib/0030030,
author = {Jasmin Blanchette and
Mark Summerfield},
title = {{C++} {GUI} Programming with Qt 4, 2nd Edition},
publisher = {Pearson Education},
year = {2008},
isbn = {978-0-13-235416-5},
timestamp = {Fri, 08 Mar 2013 00:00:00 +0100},
biburl = {https://dblp.org/rec/books/daglib/0030030.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/afp/Blanchette08,
author = {Jasmin Christian Blanchette},
title = {The Textbook Proof of Huffman's Algorithm},
journal = {Arch. Formal Proofs},
volume = {2008},
year = {2008},
url = {https://www.isa-afp.org/entries/Huffman.shtml},
timestamp = {Mon, 25 May 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/journals/afp/Blanchette08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/JohnsenBKO09,
author = {Einar Broch Johnsen and
Jasmin Christian Blanchette and
Marcel Kyas and
Olaf Owe},
editor = {Jianhua Zhao and
Volker Stolz},
title = {Intra-Object versus Inter-Object: Concurrency and Reasoning in Creol},
booktitle = {Proceedings of the 2nd International Workshop on Harnessing Theories
for Tool Support in Software, {TTSS} 2008, Istanbul, Turkey, August
30, 2008},
series = {Electronic Notes in Theoretical Computer Science},
volume = {243},
pages = {89--103},
publisher = {Elsevier},
year = {2008},
url = {https://doi.org/10.1016/j.entcs.2009.07.007},
doi = {10.1016/J.ENTCS.2009.07.007},
timestamp = {Tue, 21 Mar 2023 00:00:00 +0100},
biburl = {https://dblp.org/rec/journals/entcs/JohnsenBKO09.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{DBLP:journals/entcs/BlanchetteO08,
author = {Jasmin Christian Blanchette and
Olaf Owe},
editor = {Markus Lumpe and
Eric Madelaine},
title = {An Open System Operational Semantics for an Object-Oriented and Component-Based
Language},
booktitle = {Proceedings of the 4th International Workshop on Formal Aspects of
Component Software, {FACS} 2007, Sophia-Antipolis, France, September
19-21, 2007},
series = {Electronic Notes in Theoretical Computer Science},
volume = {215},
pages = {151--169},
publisher = {Elsevier},
year = {2007},
url = {https://doi.org/10.1016/j.entcs.2008.06.026},
doi = {10.1016/J.ENTCS.2008.06.026},
timestamp = {Mon, 20 Feb 2023 08:38:04 +0100},
biburl = {https://dblp.org/rec/journals/entcs/BlanchetteO08.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@book{DBLP:books/lib/BlanchetteS06,
author = {Jasmin Christian Blanchette and
Mark Summerfield},
title = {{C++} {GUI} programming with Qt 4},
publisher = {Prentice Hall},
year = {2006},
url = {https://www.worldcat.org/oclc/70909781},
isbn = {0131872494},
timestamp = {Fri, 17 Jul 2020 01:00:00 +0200},
biburl = {https://dblp.org/rec/books/lib/BlanchetteS06.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
a service of 
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.
last updated on 2024-02-27 23:41 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
