John Launchbury es un científico 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 emprendimiento en la implementación y aplicación de lenguajes de programación funcionales. En 2010, Launchbury fue admitido como miembro de la Association for Computing Machinery . [1]
Launchbury recibió honores de primera clase en matemáticas de la Universidad de Oxford en 1985 y una maestría. 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 Sociedad Británica de Computación . [2]
Como profesor en la Universidad de Glasgow, Launchbury centró sus primeras investigaciones en la semántica y el análisis de lenguajes funcionales perezosos y fue uno de los diseñadores contribuyentes del lenguaje de programación Haskell .
En 1993, Launchbury proporcionó una descripción formal de la evaluación diferida, abordando los desafíos al analizar 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 efectiva 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 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 eliminación de estructuras de datos intermedias [8] abordaron muchos de los desafíos de eficiencia inherentes a la evaluación diferida.
En 1994, Launchbury se mudó a la costa oeste de los Estados Unidos y en 2000 se convirtió en profesor titular en el Oregon Graduate Institute. Su investigación allí abordó la creación y optimización de lenguajes de programación de dominio específico (DSL), que van desde la investigación fundamental hasta la combinación de dispares elementos semánticos, mediante la incorporación de DSL en Haskell, hasta investigación aplicada para modelado y 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] [10] Se desempeñó como director ejecutivo 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 uso de la Agencia de Seguridad Nacional , el lenguaje se puso a disposición del público en 2008. [11]
Launchbury es titular de dos patentes sobre estructuras criptográficas en el almacenamiento de datos y una sobre mecanismos eficaces para configurar componentes criptográficos programables. [12]
En 2014, Launchbury se unió a DARPA, inicialmente como director de programas, [13] y luego como director de la Oficina de Innovación de la Información (I2O) en 2015. [9] [14] Mientras estuvo en DARPA, Launchbury dirigió programas en criptografía homomórfica (PROCEED) , ciberseguridad para vehículos y otros sistemas integrados (HACMS) y privacidad de datos (Brandeis). También definió y describió las "tres olas de la IA": conocimiento artesanal, aprendizaje estadístico y adaptación contextual. [15] [16]
En 2017, Launchbury se reincorporó a Galois como científico jefe. [17]
Launchbury publicó una perspectiva teológica sobre la interpretación del Ejemplar Moral de la doctrina de la expiación , titulada Cámbianos, no a Dios: Meditaciones bíblicas sobre la muerte de Jesús . [18]