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 de Clare College, Cambridge . [5] [6] [7] [8] [9]
Lawrence Paulson FRS | |
---|---|
Nació | Lawrence Charles Paulson 1955 (65 a 66 años) [1] |
Ciudadanía | TU APESTAS |
alma mater | |
Conocido por | |
Esposos) |
|
Premios |
|
Carrera científica | |
Campos | |
Instituciones | Universidad de Cambridge Universidad Técnica de Munich |
Tesis | Un generador de compiladores para gramáticas semánticas (1981) |
Asesor de doctorado | John L. Hennessy [6] |
Sitio web | www |
Educación
Paulson se graduó en el 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]
Investigar
Paulson llegó a la Universidad de Cambridge en 1983 y se convirtió en miembro de Clare College, Cambridge en 1987. Es mejor 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 la probadora interactiva de teoremas Isabelle , que presentó 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 licenciatura 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 este curso fue tomado por Alan Mycroft y Amanda Prorok en 2017, [19] y luego Anil Madhavapeddy y Amanda Prorok en 2019. [20] )
Premios y honores
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]
Vida personal
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]
Referencias
- ↑ a b c Anon (2017). "Paulson, Prof. Lawrence Charles" . Quién es quién . ukwhoswho.com ( edición en línea de Oxford University Press ). A & C Black, una impresión de Bloomsbury Publishing plc. doi : 10.1093 / ww / 9780199540884.013.289302 . (se requiere suscripción o membresía a una biblioteca pública del Reino Unido ) (se requiere suscripción)
- ^ a b c Anon (2017). "Profesor Lawrence Paulson FRS" . royalsociety.org . Londres: Royal Society . Consultado el 5 de mayo de 2017 .
- ^ a b Akbarpour, B .; Paulson, LC (2009). "Meti Tarski : un demostrador de teorema automático para funciones especiales de valor real". Revista de razonamiento automatizado . 44 (3): 175. CiteSeerX 10.1.1.157.3300 . doi : 10.1007 / s10817-009-9149-2 . S2CID 16215962 .
- ^ a b Anon (2008). "Profesor Lawrence C. Paulson" . awards.acm.org . Asociación de Maquinaria Informática . Consultado el 12 de abril de 2016 .
- ^ a b c d Publicaciones de Lawrence Paulson indexadas por Google Scholar
- ^ a b c Lawrence Paulson en el Proyecto de genealogía de las matemáticas
- ^ Página de perfil del autor de Lawrence Paulson en laBiblioteca digital de ACM
- ^ Lawrence C. Paulson en elservidor de bibliografía DBLP
- ^ Publicaciones de Lawrence Paulson indexadas por labase de datos bibliográfica Scopus . (requiere suscripción)
- ^ Lawrence Paulson ORCID 0000-0003-0288-4279
- ^ Paulson, Lawrence Charles (1981). Un generador de compiladores para gramáticas semánticas (PDF) . cl.cam.ac.uk (tesis doctoral). Universidad Stanford. OCLC 757240716 .
- ^ Paulson, Lawrence (1996). ML para el programador que trabaja . Cambridge Nueva York: Cambridge University Press. ISBN 978-0521565431.
- ^ "ML para el programador que trabaja" . Universidad de Cambridge . Consultado el 25 de noviembre de 2015 .
- ^ Paulson, LC (1986). "Deducción natural como resolución de orden superior". El diario de la programación lógica . 3 (3): 237–258. arXiv : cs / 9301104 . doi : 10.1016 / 0743-1066 (86) 90015-4 . S2CID 27085090 .
- ^ Paulson, Lawrence C. (1998). "El enfoque inductivo para verificar protocolos criptográficos". Revista de seguridad informática . 6 (1–2): 85–128. CiteSeerX 10.1.1.57.2049 . doi : 10.3233 / JCS-1998-61-205 . ISSN 1875-8924 .
- ^ Paulson, LC (2012). "Meti Tarski : pasado y futuro". Demostración interactiva de teoremas . Apuntes de conferencias en informática . 7406 . págs. 1-10. CiteSeerX 10.1.1.259.5577 . doi : 10.1007 / 978-3-642-32347-8_1 . ISBN 978-3-642-32346-1.
- ^ Paulson, Larry. "Lógica y prueba" . Universidad de Cambridge . Consultado el 27 de enero de 2020 .
- ^ Paulson, Larry. "Fundamentos de la informática" . Consultado el 25 de noviembre de 2015 .
- ^ "Departamento de Informática y Tecnología - Páginas del curso 2017-18: Fundamentos de la informática" . www.cl.cam.ac.uk . Consultado el 27 de enero de 2020 .
- ^ "Departamento de Informática y Tecnología - Páginas del curso 2019-20: Fundamentos de la informática" . www.cl.cam.ac.uk . Consultado el 27 de enero de 2020 .
- ^ "Certificado de nombramiento" (PDF) . TU Munich . Consultado el 12 de abril de 2016 .
- ^ Paulson, Lawrence (2010). "Susan Paulson, PhD (1959-2010)" . Universidad de Cambridge . Consultado el 25 de noviembre de 2015 .