Lawrence Charles Paulson FRS [2] (nacido en 1955) [1] es un científico informático estadounidense . Es profesor de lógica computacional en el Laboratorio de Computación de la Universidad de Cambridge y miembro del Clare College de Cambridge . [5] [6] [7] [8] [9]
Paulson se graduó del Instituto de Tecnología de California en 1977, [10] y obtuvo su doctorado en Ciencias de la Computación de la Universidad de Stanford en 1981 por su investigación sobre lenguajes de programación y compiladores-compiladores supervisados por John L. Hennessy . [6] [11]
Paulson llegó a la Universidad de Cambridge en 1983 y se convirtió en miembro de Clare College, Cambridge en 1987. Es más conocido por el texto fundamental sobre el lenguaje de programación ML , ML para el programador de trabajo . [12] [13] Su investigación se basa en el demostrador interactivo de teoremas Isabelle , que introdujo en 1986. [14] Ha trabajado en la verificación de protocolos criptográficos utilizando definiciones inductivas , [15] y también ha formalizado el universo construible de Kurt Gödel. Recientemente, ha construido un nuevo demostrador de teoremas, MetiTarski, [3] para funciones especiales de valor real. [dieciséis]
Paulson imparte un curso de pregrado en los Tripos de Ciencias de la Computación , titulado Logic and Proof [17], que cubre la demostración automatizada de teoremas y métodos relacionados. (Solía enseñar Fundamentos de la informática [18], que presenta la programación funcional , pero Alan Mycroft y Amanda Prorok se hicieron cargo de este curso en 2017, [19] y luego Anil Madhavapeddy y Amanda Prorok en 2019. [20] )
Paulson fue elegido miembro de la Royal Society (FRS) en 2017 , [2] un miembro de la Association for Computing Machinery en 2008 [4] y Profesor Afiliado Distinguido por Lógica en Informática de la Universidad Técnica de Munich . [ cuando? ] [21]
Paulson tiene dos hijos con su primera esposa, la Dra. Susan Mary Paulson, quien murió en 2010. [22] Desde 2012, está casado con la Dra. Elena Tchougounova. [1]