Грег Нельсон (ученый-компьютерщик)

Грег Нельсон
Рожденный	Чарльз Грегори Нельсон ( 1953-03-27 ) 27 марта 1953 г.
Умер	2 февраля 2015 г. (02 февраля 2015 г.) (61 год)
Образование	Бакалавр Гарвардского университета (1976 г.) Доктор философии, Стэнфордский университет (1980 г.)
Известный	Теории выполнимости по модулю Расширенная статическая проверка Проверка программы «Модула-3» комитет ESC/Java Упрощение доказательства теорем
Награды	Премия Эрбрана (2013)
Научная карьера
Учреждения	Исследовательский центр Xerox Пало-Альто (PARC) Digital Equipment Corporation (DEC) Центр системных исследований (SRC) Лаборатории Хьюлетт-Паккард
Диссертация	Методы проверки программ   (1980)
Докторантура	Роберт Тарьян

Чарльз Грегори Нельсон (27 марта 1953 — 2 февраля 2015) — американский учёный-компьютерщик .

Биография

Нельсон вырос в Гонолулу . В детстве он преуспел в гимнастике и теннисе. Он учился в университетской лабораторной школе. Он получил степень бакалавра математики в Гарвардском университете в 1976 году. Он получил степень доктора философии. Получил степень бакалавра компьютерных наук в Стэнфордском университете в 1980 году под руководством Роберта Тарьяна . Он жил в Джуно, Аляска, в течение года, прежде чем поселиться на постоянной основе в районе залива Сан-Франциско .

Заметная работа

Его диссертация «Методы верификации программ » повлиял как на верификацию программ , так и на автоматизированное доказательство теорем , особенно в области, которая теперь называется теориями выполнимости по модулю , где он внес методы комбинирования процедур принятия решений , а также эффективные процедуры принятия решений для ограничений без кванторов в логике первого порядка и алгебре термов . В 2013 году он получил премию Эрбрана :

за его новаторский вклад в доказательство теорем и верификацию программ, например, за плодотворную работу с Дереком Оппеном над сочетанием процедур выполнимости и алгоритмов быстрого конгруэнтного замыкания, за разработку весьма влиятельного средства доказательства теорем Simplify и за его роль в создании этой области расширенной статической проверки.

Он сыграл важную роль в разработке средства доказательства теорем Simplify , используемого ESC/Java . Он внес значительный вклад в ряде других областей. Он внес свой вклад в область проектирования языков программирования в качестве члена комитета Modula-3 . В распределенных системах он внес свой вклад в Network Objects. Он внес новаторский вклад, создав графические редакторы на основе ограничений (Juno и Juno-2), оконную систему (Trestle), оптимальную генерацию кода (Denali) и многопоточное программирование (Eraser).

См. также

• Список ученых-компьютерщиков
• Список программистов