Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal Scalable fine-grained proofs for formula processing. (English) Zbl 1468.68278 J. Autom. Reasoning 64, No. 3, 485-510 (2020). MSC: 68V15 PDFBibTeX XMLCite \textit{H. Barbosa} et al., J. Autom. Reasoning 64, No. 3, 485--510 (2020; Zbl 1468.68278) Full Text: DOI Link
Blanchette, Jasmin Christian; Bouzy, Aymeric; Lochbihler, Andreas; Popescu, Andrei; Traytel, Dmitriy Friends with benefits. Implementing corecursion in foundational proof assistants. (English) Zbl 1485.68280 Yang, Hongseok (ed.), 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. Berlin: Springer. Lect. Notes Comput. Sci. 10201, 111-140 (2017). MSC: 68V15 PDFBibTeX XMLCite \textit{J. C. Blanchette} et al., Lect. Notes Comput. Sci. 10201, 111--140 (2017; Zbl 1485.68280) Full Text: DOI
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef Hammering towards QED. (English) Zbl 1451.68318 J. Formaliz. Reason. 9, No. 1, 101-148 (2016). MSC: 68V15 PDFBibTeX XMLCite \textit{J. C. Blanchette} et al., J. Formaliz. Reason. 9, No. 1, 101--148 (2016; Zbl 1451.68318) Full Text: DOI
Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef A learning-based fact selector for Isabelle/HOL. (English) Zbl 1386.68149 J. Autom. Reasoning 57, No. 3, 219-244 (2016). MSC: 68T15 68T05 PDFBibTeX XMLCite \textit{J. C. Blanchette} et al., J. Autom. Reasoning 57, No. 3, 219--244 (2016; Zbl 1386.68149) Full Text: DOI Link
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy Witnessing (co)datatypes. (English) Zbl 1335.68224 Vitek, Jan (ed.), 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. Berlin: Springer (ISBN 978-3-662-46668-1/pbk; 978-3-662-46669-8/ebook). Lecture Notes in Computer Science 9032, 359-382 (2015). MSC: 68T15 68Q65 PDFBibTeX XMLCite \textit{J. C. Blanchette} et al., Lect. Notes Comput. Sci. 9032, 359--382 (2015; Zbl 1335.68224) Full Text: DOI Link
Blanchette, Jasmin Christian; Popescu, Andrei; Traytel, Dmitriy Cardinals in Isabelle/HOL. (English) Zbl 1416.68152 Klein, Gerwin (ed.) et al., 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. Berlin: Springer. Lect. Notes Comput. Sci. 8558, 111-127 (2014). MSC: 68T15 PDFBibTeX XMLCite \textit{J. C. Blanchette} et al., Lect. Notes Comput. Sci. 8558, 111--127 (2014; Zbl 1416.68152) Full Text: DOI Link
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. Extending Sledgehammer with SMT solvers. (English) Zbl 1314.68272 J. Autom. Reasoning 51, No. 1, 109-128 (2013). MSC: 68T15 PDFBibTeX XMLCite \textit{J. C. Blanchette} et al., J. Autom. Reasoning 51, No. 1, 109--128 (2013; Zbl 1314.68272) Full Text: DOI
Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef MaSh: machine learning for Sledgehammer. (English) Zbl 1317.68215 Blazy, Sandrine (ed.) et al., Interactive theorem proving. 4th international conference, ITP 2013, Rennes, France, July 22–26, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39633-5/pbk). Lecture Notes in Computer Science 7998, 35-50 (2013). MSC: 68T15 68T05 PDFBibTeX XMLCite \textit{D. Kühlwein} et al., Lect. Notes Comput. Sci. 7998, 35--50 (2013; Zbl 1317.68215) Full Text: DOI Link
Blanchette, Jasmin Christian; Paskevich, Andrei TFF1: the TPTP typed first-order form with rank-1 polymorphism. (English) Zbl 1381.68260 Bonacina, Maria Paola (ed.), Automated deduction – CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9–14, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-38573-5/pbk). Lecture Notes in Computer Science 7898. Lecture Notes in Artificial Intelligence, 414-420 (2013). MSC: 68T15 PDFBibTeX XMLCite \textit{J. C. Blanchette} and \textit{A. Paskevich}, Lect. Notes Comput. Sci. 7898, 414--420 (2013; Zbl 1381.68260) Full Text: DOI Link
Traytel, Dmitry; Popescu, Andrei; Blanchette, Jasmin C. Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. (English) Zbl 1362.68251 Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25–28, 2012. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-4769-5). 596-605 (2012). MSC: 68T15 68Q65 PDFBibTeX XMLCite \textit{D. Traytel} et al., in: Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25--28, 2012. Los Alamitos, CA: IEEE Computer Society. 596--605 (2012; Zbl 1362.68251) Full Text: DOI
Blanchette, Jasmin Christian; Krauss, Alexander Monotonicity inference for higher-order formulas. (English) Zbl 1266.03021 J. Autom. Reasoning 47, No. 4, 369-398 (2011). Reviewer: Viorica Sofronie-Stokkermans (Koblenz) MSC: 03B35 03B15 68Q60 68T15 PDFBibTeX XMLCite \textit{J. C. Blanchette} and \textit{A. Krauss}, J. Autom. Reasoning 47, No. 4, 369--398 (2011; Zbl 1266.03021) Full Text: DOI
Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. Extending Sledgehammer with SMT solvers. (English) Zbl 1314.68271 Bjørner, Nikolaj (ed.) et al., Automated deduction – CADE-23. 23rd international conference on automated deduction, Wrocław, Poland, July 31 – August 5, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22437-9/pbk; 978-3-642-22438-6/ebook). Lecture Notes in Computer Science 6803. Lecture Notes in Artificial Intelligence, 116-130 (2011). MSC: 68T15 PDFBibTeX XMLCite \textit{J. C. Blanchette} et al., Lect. Notes Comput. Sci. 6803, 116--130 (2011; Zbl 1314.68271) Full Text: DOI