Jasmin Christian Blanchette

View Scopus Profile

dr. Jasmin Christian Blanchette

 https://orcid.org/0000-0002-8367-0936
Filter
Conference contribution

Search results

  • 2023

    Recurrence-Driven Summations in Automated Deduction

    Nummelin, V., Blanchette, J. & Dahmen, S. R., 2023, Frontiers of Combining Systems: 14th International Symposium, FroCoS 2023, Prague, Czech Republic, September 20–22, 2023, Proceedings. Sattler, U. & Suda, M. (eds.). Cham: Springer Science and Business Media Deutschland GmbH, p. 23-40 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14279 LNAI).

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access
  • 2022

    Seventeen Provers Under the Hammer

    Desharnais, M., Vukmirovic, P., Blanchette, J. & Wenzel, M., 2022, 13th International Conference on Interactive Theorem Proving (ITP 2022). Andronick, J. & de Moura, L. (eds.). Dagstuhl, Germany: Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, p. 1-18 18 p. 8. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 237).

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

  • 2021

    SAT-Inspired Eliminations for Superposition

    Vukmirovic, P., Blanchette, J. & Heule, M. J. H., Oct 2021, Proceedings of the 21st Formal Methods in Computer-Aided Design - FMCAD 2021. Piskac, R., Whalen, M. W., Hunt, W. A. & Weissenbacher, G. (eds.). Institute of Electrical and Electronics Engineers Inc., p. 231-240 10 p. (Conference Series: Formal Methods in Computer-Aided Design).

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access

  • A modular Isabelle framework for verifying saturation provers

    Tourret, S. & Blanchette, J., Jan 2021, CPP 2021: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs. Hritcu, C. & Popescu, A. (eds.). Association for Computing Machinery, Inc, p. 224-237 14 p.

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access

  • A Unifying Splitting Framework

    Ebner, G., Blanchette, J. & Tourret, S., 2021, Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. Platzer, A. & Sutcliffe, G. (eds.). Springer Science and Business Media Deutschland GmbH, p. 344-360 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12699 LNAI).

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access

  • Making Higher-Order Superposition Work

    Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V. & Tourret, S., 2021, Automated Deduction – CADE 2021: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. Platzer, A. & Sutcliffe, G. (eds.). Springer Science and Business Media Deutschland GmbH, p. 415-432 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12699 LNAI).

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access

  • Superposition for Full Higher-Order Logic

    Bentkamp, A., Blanchette, J., Tourret, S. & Vukmirović, P., 2021, Automated Deduction – CADE 2021: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. Platzer, A. & Sutcliffe, G. (eds.). Springer Science and Business Media Deutschland GmbH, p. 396-412 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12699 LNAI).

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access
  • 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    84 Downloads (Pure)
  • 2019

    A verified prover based on ordered resolution

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

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    29 Downloads (Pure)

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

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

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    77 Downloads (Pure)

  • 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, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part I. 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 proceeding › Conference contribution › Academic › peer-review

    Open Access

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

    Blanchette, J., Fontaine, P., Schulz, S., Tourret, S. & Waldmann, U., 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. 1-7 7 p. (Electronic Proceedings in Theoretical Computer Science, EPTCS; vol. 311).

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-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, Natal, Brazil, August 27–30, 2019, 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    44 Downloads (Pure)
  • 2018

    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. New York, NY: Association for Computing Machinery, Inc, p. 158-171 14 p.

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    32 Downloads (Pure)

  • 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, Oxford, UK, July 14-17, 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    39 Downloads (Pure)

  • 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    41 Downloads (Pure)

  • 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, Oxford, UK, July 14-17, 2018, Proceedings. Galmiche, D., Schulz, S. & Sebastiani, R. (eds.). 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    25 Downloads (Pure)
  • 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, Brasília, Brazil, September 26–29, 2017, Proceedings. Ayala-Rincón, M. & Muñoz, C. A. (eds.). Springer, p. 46-64 19 p. (Lecture Notes in Computer Science (LNCS); vol. 10499).

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    28 Downloads (Pure)

  • A lambda-free higher-order recursive path order

    Blanchette, J. C., Waldmann, U. & Wand, D., 2017, Foundations of Software Science and Computation Structures: 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory anPractice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    5 Downloads (Pure)

  • 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, Gothenburg, Sweden, August 6–11, 2017, 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    16 Downloads (Pure)

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

    Blanchette, J. C., Fleury, M. & Weidenbach, C., 2017, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence Melbourne, Australia 19-25 August 2017. Sierra, C. (ed.). International Joint Conferences on Artificial Intelligence, AAAI Press, p. 4786-4790 5 p. (IJCAI International Joint Conference on Artificial Intelligence; vol. 0).

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    9 Downloads (Pure)

  • 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., 2017, Frontiers of Combining Systems: 11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29, 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    19 Downloads (Pure)

  • Foundational nonuniform (Co)datatypes for higher-order logic

    Blanchette, J. C., Meier, F., Popescu, A. & Traytel, D., 2017, 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS): [Proceedings]. Institute of Electrical and Electronics Engineers Inc., p. 1-12 12 p. 8005071

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    9 Downloads (Pure)

  • Friends with benefits: Implementing corecursion in foundational proof assistants

    Blanchette, J. C., Bouzy, A., Lochbihler, A., Popescu, A. & Traytel, D., 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, Uppsala, Sweden, April 22–29, 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    12 Downloads (Pure)

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

    Blanchette, J. C., Fleury, M. & Traytel, D., 2017, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017): [Proceedings]. Miller, D. (ed.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, p. 1-18 18 p. 11. (Leibniz International Proceedings in Informatics (LIPIcs); vol. 84).

    Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

    Open Access

  • 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    21 Downloads (Pure)
  • 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    20 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    123 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 proceeding › Conference contribution › Academic › peer-review

    Open Access
    File
    22 Downloads (Pure)