John Launchbury es un informático estadounidense y británico que actualmente es científico jefe en Galois, Inc. Anteriormente, dirigió una de las oficinas técnicas de DARPA , donde supervisó la investigación científica y de ingeniería a escala nacional en ciberseguridad , análisis de datos e inteligencia artificial . Es conocido por la investigación y el espíritu empresarial en la implementación y aplicación de lenguajes de programación funcionales. En 2010, Launchbury fue admitida como miembro de la Association for Computing Machinery . [1]
Educación
Launchbury recibió honores de primera clase en matemáticas de la Universidad de Oxford en 1985, y un M.Sc. en Computación en 1986. Tiene un Ph.D. en ciencias de la computación de la Universidad de Glasgow . En 1991, Cambridge University Press publicó su tesis, Factorizaciones de proyección en evaluación parcial , después de ganar el distinguido premio de disertación de la British Computer Society . [2]
Carrera e investigación
Como profesor en la Universidad de Glasgow, Launchbury centró sus primeras investigaciones en la semántica y el análisis de los lenguajes funcionales perezosos y fue uno de los diseñadores que contribuyeron al lenguaje de programación Haskell .
En 1993, Launchbury proporcionó una descripción formal de la evaluación perezosa, abordando los desafíos en el análisis de los requisitos de almacenamiento de un programa. [3] La semántica operativa se cita ampliamente en investigaciones posteriores sobre Haskell. En el contexto del equipo Glasgow Haskell Compiler, [4] Launchbury estableció una asociación eficaz con Simon L. Peyton Jones para escribir una serie de artículos que influyeron dramáticamente en el diseño de Haskell. Su artículo de 1995 sobre el Estado en Haskell [5] introdujo la “ mónada IO ” como una forma práctica matemáticamente limpia de expresar efectos en el mundo externo, y solidificó la “ notación do ” que Launchbury había introducido anteriormente. [6] Sus artículos sobre valores sin caja [7] y la eliminación de estructuras de datos intermedias [8] abordaron muchos de los desafíos de eficiencia inherentes a la evaluación perezosa.
En 1994, Launchbury se trasladó a la costa oeste de los Estados Unidos y se convirtió en profesor titular en el Oregon Graduate Institute en 2000. Su investigación allí abordó la creación y optimización de lenguajes de programación específicos de dominio (DSL) que van desde la investigación fundamental hasta la combinación de diferentes elementos semánticos, a través de la incorporación de DSL en Haskell, a la investigación aplicada para el modelado y el razonamiento sobre microarquitecturas de integración a muy gran escala (VLSI) .
Launchbury fundó Galois Inc. en 1999 para abordar los desafíos en el aseguramiento de la información mediante la aplicación de programación funcional y métodos formales. [9] Se desempeñó como CEO y Científico Jefe de la compañía de 2000 a 2014. Bajo la dirección de Launchbury, Galois Inc. desarrolló el lenguaje específico del dominio Cryptol para especificar y verificar implementaciones criptográficas. Originalmente diseñado para su uso por la Agencia de Seguridad Nacional , el idioma se puso a disposición del público en 2008. [10]
Launchbury es titular de dos patentes sobre estructuras criptográficas en el almacenamiento de datos y una sobre mecanismos efectivos para configurar componentes criptográficos programables. [11]
En 2014, Launchbury se unió a DARPA, inicialmente como gerente de programas, y luego como director de la Oficina de Innovación de la Información (I2O) en 2015. [9] Launchbury dirigió programas en criptografía homomórfica ( PROCEED ), ciberseguridad para vehículos y otros sistemas integrados ( HACMS) ) y privacidad de datos ( Brandeis ).
En 2017, Launchbury se reincorporó a Galois como científico jefe.
Otras publicaciones
Launchbury publicó una perspectiva teológica sobre la interpretación Moral Ejemplar de la doctrina de la expiación , titulada Cambienos, no Dios: Meditaciones bíblicas sobre la muerte de Jesús . [12]
Referencias
- ^ "Becarios de ACM" . Premios ACM . Asociación de Maquinaria Informática . Consultado el 21 de septiembre de 2016 .
- ^ Launchbury, John (1991). Factorizaciones de proyección en evaluación parcial . Nueva York, NY, EE.UU .: Cambridge University Press. pag. 163. ISBN 978-0-521-41497-5.
- ^ Launchbury, John (1993). "Una semántica natural para la evaluación perezosa" (PDF) . Actas del vigésimo simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación - POPL '93 . Académico semántico . ACM. págs. 144-154. doi : 10.1145 / 158511.158618 . ISBN 0897915607. S2CID 14945994 . Consultado el 19 de enero de 2017 .
- ^ "El equipo de Glasgow Haskell: otros maravillosos colaboradores anteriores" . La computadora Glasgow Haskell . Consultado el 30 de noviembre de 2016 .
- ^ Launchbury, John; Jones, Simon L Peyton (1 de diciembre de 1995). Estado en Haskell (PDF) . Boston, MA: Kluwer Academic Publishers. pag. 51.
- ^ Launchbury, John. "Programación imperativa perezosa" . CiteSeerX . Universidad de Yale . Consultado el 19 de enero de 2017 .
- ^ Simon L Peyton Jones ; John Launchbury (1991). Valores sin caja como ciudadanos de primera en un lenguaje funcional no estricto . Nueva York, NY, EE.UU .: Springer-Verlag New York, Inc. págs. 145–164. ISBN 978-0-387-54396-3.
- ^ Andrew Gill; John Launchbury; Simon L Peyton Jones (junio de 1993). Un atajo a la deforestación (PDF) . Copenhague, Dinamarca: Conferencia FPCA '93 Conferencia sobre lenguajes de programación funcionales y arquitectura informática.
- ^ a b "Dr. John Launchbury" . Página de inicio de DARPA . DARPA . Consultado el 21 de septiembre de 2016 .
- ^ Galois, Inc (24 de diciembre de 2008). "Cryptol, el lenguaje de la criptografía, ahora disponible" . Galois.com . Consultado el 30 de noviembre de 2016 .
- ^ "Patentes del inventor John Launchbury" . Patentes Justia .
- ^ John Launchbury (1 de agosto de 2009). Cambianos a nosotros, no a Dios . Publicación WCF. pag. 200. ISBN 978-0982409299.