Greg Nelson (computer scientist)

{{Infobox scientist

| name = Greg Nelson

| birth_name = Charles Gregory Nelson

| birth_date = {{birth date |1953|03|27}}

| death_date = {{death date and age |2015|02|02 |1953|03|01}}

| workplaces = Xerox Palo Alto Research Center (PARC)
Digital Equipment Corporation (DEC) Systems Research Center (SRC)
Hewlett-Packard Labs

| education = B.A., Harvard University (1976)
Ph.D., Stanford University (1980)

| thesis_title = Techniques for Program Verification

| thesis_url = http://people.eecs.berkeley.edu/~necula/Papers/nelson-thesis.pdf

| thesis_year = 1980

| doctoral_advisor = Robert Tarjan

| known_for = Satisfiability modulo theories
Extended static checking
Program verification
Modula-3 committee
ESC/Java Simplify theorem prover

| awards = Herbrand Award (2013)

}}

Charles Gregory Nelson (27 March 1953 – 2 February 2015) was an American computer scientist.

{{cite news |last=Perl |first=Sharon |date=February 2015 |url=https://www.paloaltoonline.com/obituaries/memorials/greg-nelson?o=4203 |title=Greg Nelson: 27 March 1953 – 2 February 2015 |work=Palo Alto Online |location=Palo Alto, California |access-date=2021-04-15}}

{{cite news |last=Perl |first=Sharon |date=March 4, 2015 |url=http://obits.staradvertiser.com/2015/03/04/greg-nelson/ |title=Greg Nelson |work=Honolulu Star-Advertiser: Obituaries |location=Honolulu, Hawaii |access-date=2021-04-15}}

Biography

Nelson grew up in Honolulu. As a boy he excelled at gymnastics and tennis. He attended the University Laboratory School. He received his B.A. degree in mathematics from Harvard University in 1976. He received his Ph.D. in computer science from Stanford University in 1980 under the supervision of Robert Tarjan. He lived in Juneau, Alaska for a year before settling permanently in the San Francisco Bay Area.

Notable work

His thesis, Techniques for Program Verification,{{cite thesis |type=PhD |last=Nelson |first=Greg |date=1980–1981 |title=Techniques for Program Verification |url=http://people.eecs.berkeley.edu/~necula/Papers/nelson-thesis.pdf |website=Department of Electrical Engineering and Computer Sciences |publisher=University of California Berkeley |access-date=2021-04-13}} influenced both program verification and automated theorem proving, especially in the area now named satisfiability modulo theories, where he contributed techniques for combining decision procedures, as well as efficient decision procedures for quantifier-free constraints in first-order logic and term algebra. He received the Herbrand Award in 2013:{{cite news |last1=Montmirail |first1=Valentin |last2=Sutcliffe |first2=Geoff |date=June 2013 |title=Herbrand Award: for Distinguished Contributions to Automated Reasoning |url=http://www.cadeinc.org/Herbrand-Award |website=Conference on Automated Deduction |access-date=2021-04-13}}

{{Blockquote|for his pioneering contributions to theorem proving and program verification, such as his seminal work with Derek Oppen on the combination of satisfiability procedures and fast congruence closure algorithms, the development of the highly influential theorem prover Simplify, and his role in the creation of the field of extended static checking.}}

He was instrumental in developing the Simplify theorem prover used by ESC/Java. He made significant contributions in several other areas. He contributed to the field of programming language design as a member of the Modula-3 committee. In distributed systems he contributed to Network Objects. He made pioneering contributions with his constraint-based graphics editors (Juno and Juno-2), windowing system (Trestle), optimal code generation (Denali), and multi-threaded programming (Eraser).