Lawrence Paulson
Lawrence Paulson | |
|---|---|
 Paulson en 2017 | |
| Nacido | Lawrence Charles Paulson 1955 (68-69 años) [4] |
| Ciudadanía | Estados Unidos/Reino Unido |
| Alma máter | |
| Conocido por | |
| Esposas |
|
| Premios |
|
| Carrera científica | |
| Campos | |
| Instituciones | Universidad de Cambridge Universidad Técnica de Múnich |
| Tesis | Un generador de compiladores para gramáticas semánticas (1981) |
| Asesor de doctorado | Juan L. Hennessy [3] |
| Sitio web | www.cl.cam.ac.uk/~lp15/ |
Lawrence Charles Paulson 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 de Cambridge . [2] [3] [7] [8] [9]
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 en la Universidad de Stanford en 1981 por su investigación sobre lenguajes de programación y compiladores supervisados por John L. Hennessy . [3] [11]
Investigación
Paulson llegó 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 demostrador de teoremas interactivo 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, [6] para funciones especiales de valor real. [16]
Paulson imparte un curso de conferencias de pregrado en el programa Tripos de Ciencias de la Computación , titulado Lógica y Demostración [17], que cubre la demostración automatizada de teoremas y métodos relacionados. (Solía enseñar Fundamentos de Ciencias de la Computación [18] , que introduce la programación funcional , pero este curso fue asumido por Alan Mycroft y Amanda Prorok en 2017, [19] y luego por Anil Madhavapeddy y Amanda Prorok en 2019. [20] )
Premios y honores
Paulson fue elegido miembro de la Royal Society (FRS) en 2017 , [5] miembro de la Association for Computing Machinery en 2008 [1] y profesor afiliado distinguido de lógica en informática en la Universidad Técnica de Múnich . [ ¿cuándo? ] [21]
Vida personal
Paulson tiene dos hijos con su primera esposa, la Dra. Susan Mary Paulson, quien falleció en 2010. [22] Desde 2012, está casado con la Dra. Elena Tchougounova. [4]
Referencias
- ^ ab Anon (2008). "Profesor Lawrence C. Paulson". awards.acm.org . Association for Computing Machinery . Consultado el 12 de abril de 2016 .
- ^ abcd Publicaciones de Lawrence Paulson indexadas por Google Scholar
- ^ abc Lawrence Paulson en el Proyecto de Genealogía Matemática
- ^ ab Anónimo (2017). "Paulson, Prof. Lawrence Charles" . Quién es quién (edición en línea de Oxford University Press ). Oxford: A & C Black. doi :10.1093/ww/9780199540884.013.289302. (Se requiere suscripción o membresía a una biblioteca pública del Reino Unido).
- ^ ab Anon (2017). "Profesor Lawrence Paulson FRS". royalsociety.org . Londres: Royal Society . Consultado el 5 de mayo de 2017 .
- ^ ab Akbarpour, B.; Paulson, LC (2009). "Meti Tarski : Un demostrador automático de teoremas 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.
- ^ Página de perfil del autor Lawrence Paulson en la Biblioteca Digital ACM
- ^ Lawrence C. Paulson en el servidor de bibliografía DBLP
- ^ Publicaciones de Lawrence Paulson indexadas en la base 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 de 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 en activo". Universidad de Cambridge . Consultado el 25 de noviembre de 2015 .
- ^ Paulson, LC (1986). "Deducción natural como resolución de orden superior". The Journal of Logic Programming . 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". Journal of Computer Security . 6 (1–2): 85–128. arXiv : 2105.06319 . CiteSeerX 10.1.1.57.2049 . doi :10.3233/JCS-1998-61-205. ISSN 1875-8924. S2CID 7591720.
- ^ Paulson, LC (2012). "Meti Tarski : Pasado y futuro". Demostración interactiva de teoremas . Apuntes de clase en informática . Vol. 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 demostración". 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 Ciencias de la Computación 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 Ciencias de la Computación 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) . Universidad Técnica de Múnich . 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 .
 | Este artículo biográfico sobre un informático es un esbozo . Puedes ayudar a Wikipedia expandiéndolo. |
