Find Research outputs

Search in all content

Filters for Research output

Search concepts
Selected filters

Publication Year

  • 2019
  • 2018
  • 2012

Author

  • Jasmin Christian Blanchette
  • 14 results
  • Export search results

Search results

  • Editorial

    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, p. 1-8 8 p.

    Research output: Contribution to JournalEditorialAcademicpeer-review

    Open Access
    File
    28 Downloads (Pure)
  • 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

    Open Access
    File
    12 Downloads (Pure)
  • Selected Extended Papers of ITP 2016: Preface

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

    Research output: Contribution to JournalEditorialAcademicpeer-review

    Open Access
    File
    22 Downloads (Pure)
  • Conference contribution

    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

  • 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

  • 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 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

  • 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

  • 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 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

  • 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

  • Article

    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 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