John Harrison realiza verificação formal na Intel Corporation. Ele se especializou principalmente em verificação de algoritmos de ponto flutuante e de outros softwares matemáticos, mas ele se interessa por todos os aspectos de prova e verificação de teoremas. Ele também se interessa pela própria aritmética de ponto flutuante em si, tendo contribuido para o processo de revisão que conduziu ao novo padrão IEEE 754 de ponto flutuante. Antes de ingressar na Intel em 1998, ele foi membro do Grupo de Raciocínio Automatizado no Laboratório de Computação da Universidade de Cambridge. Ele trabalhou como um Pesquisador Associado e estudante de doutorado lá, sob a orientação de Mike Gordon e, depois de um período de um ano no Departamento de Ciência da Computação da Universidade da Academia de Åbo na Finlândia, retornou para Cambridge como um Pesquisador Associado trabalhando em Verificação de Ponto Flutuante.

Ele tem ajudado na organização de várias conferências importantes na área de ciência da computação, sendo a mais recente delas a conferência IEEE ARITH (computer arithmetic) em Portland, OR. Ele é um participante regular em uma ampla gama de eventos acadêmicos, e é o autor do livro recentemente publicado "Handbook of Practical Logic and Automated Reasoning". Ele é um membro do corpo editorial do periódico "the Journal of Automated Reasoning".

Para mais detalhes, visite sua home page.