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
Recursive functions
Engineering & Materials Science
Superposition
Mathematics
Functional programming
Engineering & Materials Science
Syntactics
Engineering & Materials Science
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
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., 1 Jan 2019, (Accepted/In press) In : Journal of Automated Reasoning.Research output: Contribution to Journal › Article › Academic › peer-review
Surface mount technology
Data structures
Processing
A Formal Proof of the Expressiveness of Deep Learning
Bentkamp, A., Blanchette, J. C. & Klakow, D., 22 Sep 2018, (Accepted/In press) In : Journal of Automated Reasoning. p. 1-22 22 p.Research output: Contribution to Journal › Article › Academic › peer-review
Image recognition
Bioinformatics
Computer science
Tensors
Polynomials
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, p. 1-33 33 p.Research output: Contribution to Journal › Article › Academic › peer-review
Open Access
Functional programming
Computer programming languages
Data structures
Concretes
Experiments