About me
Name: Dr. Paul Jackson
Title: Senior Lecturer (Associate Professor)
Affiliation: School of Informatics, University of Edinburgh
Bio:
My research interests concern the development of formal verification
tools and their application in such domains as digital hardware,
software, cyber-physical systems and formalised mathematics. Recently
my focus has been on applications of the Lean 4 proof assistant. A
proof assistant is a computer environment in which mathematical
definitions, theorems and proofs can be expressed, developed and
checked in a completely formal way. My former PhD student Ramon
Fernandez-Mir applied Lean to transforming Disciplined Convex
Programming problems into conic form. One current interest is in
verifying compiler optimisations targeting linear algebra computations
and database queries.
