dr. Jasmin Christian Blanchette

    20162020

    Research output per year

    If you made any changes in Pure these will be visible here soon.

    Research Output

    2020

    A Comprehensive Framework for Saturation Theorem Proving

    Waldmann, U., Tourret, S., Robillard, S. & Blanchette, J., 2020, Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I. Peltier, N. & Sofronie-Stokkermans, V. (eds.). Springer, Vol. 1. p. 316-334 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12166 LNAI).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

    Schlichtkrull, A., Blanchette, J., Traytel, D. & Waldmann, U., Oct 2020, In : Journal of Automated Reasoning. 64, 7, p. 1169-1195 27 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Scalable Fine-Grained Proofs for Formula Processing

    Barbosa, H., Blanchette, J. C., Fleury, M. & Fontaine, P., Mar 2020, In : Journal of Automated Reasoning. 64, 3, p. 485-510

    Research output: Contribution to JournalArticleAcademicpeer-review

    2019

    A Formal Proof of the Expressiveness of Deep Learning

    Bentkamp, A., Blanchette, J. C. & Klakow, D., Aug 2019, In : Journal of Automated Reasoning. 63, 2, p. 347-368 22 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access

    A verified prover based on ordered resolution

    Schlichtkrull, A., Blanchette, J. C. & Traytel, D., 14 Jan 2019, CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. Mahboubi, A. (ed.). Association for Computing Machinery, Inc, p. 152-165 14 p.

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Extending a brainiac prover to lambda-free higher-order logic

    Vukmirović, P., Blanchette, J. C., Cruanes, S. & Schulz, S., 2019, 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, Proceedings - Part 1. Zhang, L. & Vojnar, T. (eds.). Springer Verlag, Vol. 1. p. 192-210 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11427 LNCS).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)

    Blanchette, J. C., 14 Jan 2019, CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. Mahboubi, A. (ed.). Association for Computing Machinery, Inc, p. 1-13 13 p.

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Introduction to the STAF 2015 special section

    Blanchette, J., Bordeleau, F., Pierantonio, A., Kosmatov, N., Taentzer, G. & Wimmer, M., 8 Feb 2019, In : Software and Systems Modeling. 18, 1, p. 191-193 3 p.

    Research output: Contribution to JournalEditorialAcademicpeer-review

    Scalable Fine-Grained Proofs for Formula Processing

    Barbosa, H., Blanchette, J. C., Fleury, M. & Fontaine, P., 4 Jan 2019, In : Journal of Automated Reasoning. 64, 3, p. 1-26 26 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Selected Extended Papers of ITP 2016: Preface

    Blanchette, J. C. & Merz, S., Feb 2019, In : Journal of Automated Reasoning. 62, 2, p. 169-170 2 p.

    Research output: Contribution to JournalEditorialAcademicpeer-review

    Stronger higher-order automation: A report on the ongoing MatryoShka project

    Blanchette, J., Fontaine, P., Schulz, S., Tourret, S. & Waldmann, U., 31 Dec 2019, EPTCS 311: Proceedings of the Second International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements - Natal, Brazil, August 26, 2019. Suda, M. & Winkler, S. (eds.). EPTCS, p. 11-18 8 p. (Electronic Proceedings in Theoretical Computer Science, EPTCS; vol. 311).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Open Access

    Superposition with lambdas

    Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P. & Waldmann, U., 2019, Automated Deduction – CADE 2019: 27th International Conference on Automated Deduction, Proceedings. Fontaine, P. (ed.). Springer, p. 55-73 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11716 LNAI).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    2018

    A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

    Blanchette, J. C., Fleury, M., Lammich, P. & Weidenbach, C., 12 Mar 2018, In : Journal of Automated Reasoning. 2018, 1-4, p. 1-33 33 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access

    A verified SAT solver with watched literals using Imperative HOL

    Fleury, M., Blanchette, J. C. & Lammich, P., Jan 2018, CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018. New York, NY: Association for Computing Machinery, Inc, p. 158-171 14 p.

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

    Schlichtkrull, A., Blanchette, J. C., Traytel, D. & Waldmann, U., 2018, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, p. 89-107 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Introduction to Milestones in Interactive Theorem Proving

    Avigad, J., Blanchette, J. C., Klein, G., Paulson, L., Popescu, A. & Snelting, G., Jun 2018, In : Journal of Automated Reasoning. 61, 1-4, p. 1-8 8 p.

    Research output: Contribution to JournalEditorialAcademicpeer-review

    Superposition for Lambda-Free Higher-Order Logic

    Bentkamp, A., Blanchette, J. C., Cruanes, S. & Waldmann, U., 2018, 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. Galmiche, D., Schulz, S. & Sebastiani, R. (eds.). Springer/Verlag, p. 28-46 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Superposition with Datatypes and Codatatypes

    Blanchette, J. C., Peltier, N. & Robillard, S., 2018, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, p. 370-387 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    2017

    A formal proof of the expressiveness of deep learning

    Bentkamp, A., Blanchette, J. C. & Klakow, D., 2017, Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017, Proceedings. Springer, Vol. 10499. p. 46-64 (LNCS).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    A lambda-free higher-order recursive path order

    Blanchette, J. C., Waldmann, U. & Wand, D., 1 Jan 2017, 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, Proceedings. Esparza, J. & Murawski, A. S. (eds.). Springer/Verlag, p. 461-479 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10203 LNCS).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    An Isabelle Formalization of the Expressiveness of Deep Learning (Extended Abstract)

    Bentkamp, A., Blanchette, J. C. & Klakow, D., 2017, p. 22-23. 2 p.

    Research output: Contribution to ConferenceAbstractOther research output

    A transfinite knuth–bendix order for lambda-free higher-order terms

    Becker, H., Blanchette, J. C., Waldmann, U. & Wand, D., 2017, Automated Deduction - CADE 26: 26th International Conference on Automated Deduction, Proceedings. de Moura, L. (ed.). Springer/Verlag, p. 432-453 22 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10395 LNAI).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    A verified SAT solver framework with learn, forget, restart, and incrementality

    Blanchette, J. C., Fleury, M. & Weidenbach, C., 1 Jan 2017, 26th International Joint Conference on Artificial Intelligence, IJCAI 2017. Sierra, C. (ed.). International Joint Conferences on Artificial Intelligence, AAAI Press, p. 4786-4790 5 p.

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Open Access

    Foundational (co)datatypes and (co)recursion for higher-order logic

    Biendarra, J., Blanchette, J. C., Bouzy, A., Desharnais, M., Fleury, M., Hölzl, J., Kunčar, O., Lochbihler, A., Meier, F., Panny, L., Popescu, A., Sternagel, C., Thiemann, R. & Traytel, D., 1 Jan 2017, Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings. Dixon, C. & Finger, M. (eds.). Springer/Verlag, p. 3-21 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10483 LNAI).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Foundational nonuniform (Co)datatypes for higher-order logic

    Blanchette, J. C., Meier, F., Popescu, A. & Traytel, D., 8 Aug 2017, 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017. Institute of Electrical and Electronics Engineers Inc., 8005071

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Friends with benefits: Implementing corecursion in foundational proof assistants

    Blanchette, J. C., Bouzy, A., Lochbihler, A., Popescu, A. & Traytel, D., 1 Jan 2017, 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, Proceedings. Yang, H. (ed.). Springer/Verlag, p. 111-140 30 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10201 LNCS).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Language and Proofs for Higher-Order SMT (Work in Progress)

    Barbosa, H., Blanchette, J. C., Cruanes, S., El Ouraoui, D. & Fontaine, P., 2017, In : Electronic Proceedings in Theoretical Computer Science. 262, 262, p. 15-22 8 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access

    Nested multisets, hereditary multisets, & syntactic ordinals in Isabelle/HOL

    Blanchette, J. C., Fleury, M. & Traytel, D., 1 Sep 2017, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017. Miller, D. (ed.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Vol. 84. 11

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Scalable fine-grained proofs for formula processing

    Barbosa, H., Blanchette, J. C. & Fontaine, P., 2017, Automated Deduction: CADE 26 - 26th International Conference on Automated Deduction, Proceedings. de Moura, L. (ed.). Springer/Verlag, p. 398-412 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10395 LNAI).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Soundness and Completeness Proofs by Coinductive Methods

    Blanchette, J. C., Popescu, A. & Traytel, D., Jan 2017, In : Journal of Automated Reasoning. 58, 1, p. 149-179 31 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    2016

    A Decision Procedure for (Co)datatypes in SMT Solvers

    Reynolds, A. & Blanchette, J. C., 2016, Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence: IJCAI 2016, New York, NY, USA, 9-15 July 2016. IJCAI/AAAI Press, p. 4205-4209

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Open Access
    File
    7 Downloads (Pure)

    A Learning-Based Fact Selector for Isabelle/HOL

    Blanchette, J. C., Greenaway, D., Kaliszyk, C., Kühlwein, D. & Urban, J., 1 Oct 2016, In : Journal of Automated Reasoning. 57, 3, p. 219-244 26 p.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access
    File
    90 Downloads (Pure)

    A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

    Blanchette, J. C., Fleury, M. & Weidenbach, C., 2016, Automated Reasoning - 8th International Joint Conference: IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. Springer, p. 25-44 (Lecture Notes in Computer Science; vol. 9706).

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Open Access
    File
    92 Downloads (Pure)

    Encoding Monomorphic and Polymorphic Types

    Blanchette, J. C., Böhme, S., Popescu, A. & Smallbone, N., 2016, In : Logical Methods in Computer Science.

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access
    File
    6 Downloads (Pure)

    Hammering towards QED

    Blanchette, J. C., Kaliszyk, C., Paulson, L. C. & Urban, J., 2016, In : Journal of Formalized Reasoning. 9, 1, p. 101-148

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access
    File
    57 Downloads (Pure)

    Model Finding for Recursive Functions in SMT

    Reynolds, A., Blanchette, J. C., Cruanes, S. & Tinelli, C., 2016, Automated Reasoning - 8th International Joint Conference: IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. Springer, p. 133-151

    Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

    Open Access
    File
    2 Downloads (Pure)

    Semi-intelligible Isar Proofs from Machine-Generated Proofs

    Blanchette, J. C., Böhme, S., Fleury, M., Smolka, S. J. & Steckermeier, A., 2016, In : Journal of Automated Reasoning. p. 155-200

    Research output: Contribution to JournalArticleAcademicpeer-review

    Open Access
    File
    10 Downloads (Pure)