Charles Gregory Nelson (27 marzo 1953-2 febrero 2015) fue un estadounidense experto en informática . [1] [2]
Greg Nelson | |
---|---|
Nació | Charles Gregory Nelson 27 de marzo de 1953 |
Fallecido | 2 de febrero de 2015 | (61 años)
Educación | Licenciatura, Universidad de Harvard (1976) Doctorado, Universidad de Stanford (1980) |
Conocido por | Teorías del módulo de satisfacción Verificación estática extendida Verificación del programa Comité Modula-3 ESC / Java Demostrador de teoremas de simplificación |
Premios | Premio Herbrand (2013) |
Carrera científica | |
Instituciones | Xerox Palo Alto Research Center (PARC) Digital Equipment Corporation (DEC) Systems Research Center (SRC) Hewlett-Packard Labs |
Tesis | Técnicas para la verificación de programas (1980) |
Asesor de doctorado | Robert Tarjan |
Biografía
Nelson creció en Honolulu . De niño se destacó en gimnasia y tenis. Asistió a la Escuela de Laboratorio de la Universidad. Recibió su licenciatura en matemáticas de la Universidad de Harvard en 1976. Recibió su Ph.D. en Ciencias de la Computación de la Universidad de Stanford en 1980 bajo la supervisión de Robert Tarjan . Vivió en Juneau, Alaska durante un año antes de establecerse permanentemente en el Área de la Bahía de San Francisco .
Trabajo notable
Su tesis, Técnicas para la verificación de programas , [3] influyó tanto en la verificación de programas como en la demostración automatizada de teoremas , especialmente en el área ahora llamada teorías de módulo de satisfacibilidad , donde contribuyó con técnicas para combinar procedimientos de decisión , así como procedimientos de decisión eficientes para restricciones sin cuantificadores en lógica de primer orden y álgebra de términos . Recibió el premio Herbrand en 2013: [4]
por sus contribuciones pioneras a la demostración de teoremas y la verificación de programas, como su trabajo seminal con Derek Oppen sobre la combinación de procedimientos de satisfacibilidad y algoritmos rápidos de cierre de congruencia, el desarrollo del altamente influyente demostrador de teoremas Simplify y su papel en la creación del campo de comprobación estática ampliada.
Jugó un papel decisivo en el desarrollo del demostrador del teorema Simplify utilizado por ESC / Java . Hizo contribuciones significativas en varias otras áreas. Contribuyó al campo del diseño de lenguajes de programación como miembro del comité Modula-3 . En sistemas distribuidos contribuyó a Network Objects. Hizo contribuciones pioneras con sus editores gráficos basados en restricciones (Juno y Juno-2), sistema de ventanas (caballete), óptima generación de código (Denali), y multi- roscado programación (Borrador).
Ver también
Referencias
- ^ Perl, Sharon (febrero de 2015). "Greg Nelson: 27 de marzo de 1953 - 2 de febrero de 2015" . Palo Alto en línea . Palo Alto , California . Consultado el 15 de abril de 2021 .
- ^ Perl, Sharon (4 de marzo de 2015). "Greg Nelson" . Honolulu Star-Advertiser: obituarios . Honolulu , Hawái . Consultado el 15 de abril de 2021 .
- ^ Nelson, Greg (1980-1981). Técnicas para la verificación de programas (PDF) . Departamento de Ingeniería Eléctrica y Ciencias de la Computación (PhD). Universidad de California Berkeley . Consultado el 13 de abril de 2021 .
- ^ Montmirail, Valentin; Sutcliffe, Geoff (junio de 2013). "Premio Herbrand: por contribuciones distinguidas al razonamiento automatizado" . Conferencia sobre Deducción Automatizada . Consultado el 13 de abril de 2021 .