Research Output per year
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 (Sledgehammer, Nitpick, Nunchaku, 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
NWO Vidi 2017
Lean Forward: Usable Computer-Checked Proofs and Computations for Number Theorists
ERC Starting Grant 2016
Matryoshka: Fast Interactive Verification through Strong Higher-Order Automation
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 proceeding › Conference contribution › Academic › peer-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 proceeding › Conference contribution › Academic › peer-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 proceeding › Conference contribution › Academic › peer-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 Journal › Article › Academic › peer-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 Journal › Editorial › Academic › peer-review