Email: jose.divason at


I studied Computer Science and Mathematics at Universidad de La Rioja from October 2007 to June 2011. Until June 2012 I was working as an assistant researcher in the ForMath Project.

From July 2012 to June 2016, I was a Ph.D student supervised by Dr. Julio Rubio and Dr. Jesús Aransay at Universidad de La Rioja. My thesis mostly is related to the formalisation of Linear Algebra algorithms in Higher-Order Logic. From 2016, I am a lecturer at the same university.


Some of my research interests are:

  • Interactive theorem proving
  • Formalization of mathematics
  • Verification of algorithms
  • Formal methods
  • Lattice-based cryptography and post-quantum cryptography

Most of my current work is carried out using the Isabelle theorem prover. Some of our developments using this theorem prover are shown here. A list of our publications can be found here.

Jose Divasón - Free Website Template by Derby Web Design