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

Personal profile

Personal information

I am an assistant professor in the Theoretical Computer Science section of the Vrije Universiteit Amsterdam, in the Netherlands. I am also a guest researcher in the VeriDisgroup at Loria in Nancy, France, and in the Automation of Logic group at the Max-Planck-Institut für Informatik in Saarbrücken, Germany. I was a postdoc at the Chair for Logic and Verification at the Technische Universität München, Germany, which I joined in 2008 as a PhD student. From 2000 to 2008, I worked as software engineer and documentation manager for Trolltech (now The Qt Company) in Oslo, Norway.

Research

My research focuses on the use of first-order automatic theorem provers and model finders to find proofs and counterexamples in higher-order logic (SledgehammerNitpickNunchaku, and Matryoshka). Another aspect of my work is the development of foundational definitional mechanisms for (co)datatypes and (co)recursive functions. I am also interested in formalizing classic results and modern research in automated reasoning (IsaFoL) and number theory (Lean Forward).

Grants

Ancillary activities

No ancillary activities

Ancillary activities are updated daily

Fingerprint Fingerprint is based on mining the text of the person's scientific documents to create an index of weighted terms, which defines the key subjects of each individual researcher.

  • 2 Similar Profiles
Data structures Engineering & Materials Science
Higher-order Logic Mathematics
Surface mount technology Engineering & Materials Science
Superposition Mathematics
Recursive functions Engineering & Materials Science
Functional programming Engineering & Materials Science
Higher Order Mathematics
Calculus Mathematics

Network Recent external collaboration on country level. Dive into details by clicking on the dots.

Research Output 2016 2019

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

Specifications

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

Higher-order Logic
Data structures
Algorithms and Data Structures
Higher Order
Theorem proving

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

Scalable Fine-Grained Proofs for Formula Processing

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

Research output: Contribution to JournalArticleAcademicpeer-review

Surface mount technology
Data structures
Processing

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