Lawrence Charles Paulson FRS [2] (nacido en 1955) [1] es un 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, 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 en lenguajes de programación y compiladores-compiladores supervisados por John L. Hennessy . [6] [11]
Paulson ingresó a la Universidad de Cambridge en 1983 y se convirtió en miembro del Clare College de Cambridge en 1987. Es más conocido por el texto fundamental sobre el lenguaje de programación ML , ML for the Working Programmer . [12] [13] Su investigación se basa en el probador 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 Godel. Recientemente ha construido un nuevo probador de teoremas, MetiTarski, [3] para funciones especiales de valor real. [dieciséis]
Paulson imparte un curso de conferencias de pregrado en Ciencias de la Computación Tripos , titulado Lógica y prueba [17] que cubre la prueba automatizada de teoremas y métodos relacionados. (Solía enseñar Fundamentos de la informática [18], que introduce 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] miembro de la Association for Computing Machinery en 2008 [4] y profesor afiliado distinguido de lógica en informática en la Universidad Técnica de Munich . [ ¿cuándo? ] [21]
Paulson tiene dos hijos de su primera esposa, la Dra. Susan Mary Paulson, quien murió en 2010. [22] Desde 2012, está casado con la Dra. Elena Tchougounova. [1]