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

computer scientist A computer scientist is a person who is trained in the academic study of computer science. Computer scientists typically work on the theoretical side of computation, as opposed to the hardware side on which computer engineers mainly focus ( ...

Biography

Nelson grew up in

Honolulu Honolulu (; ) is the capital and largest city of the U.S. state of Hawaii, which is in the Pacific Ocean. It is an unincorporated county seat of the consolidated City and County of Honolulu, situated along the southeast coast of the islan ...

. 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 Harvard University is a private Ivy League research university in Cambridge, Massachusetts. Founded in 1636 as Harvard College and named for its first benefactor, the Puritan clergyman John Harvard, it is the oldest institution of high ...

in 1976. He received his Ph.D. in computer science from Stanford University in 1980 under the supervision of

Robert Tarjan Robert Endre Tarjan (born April 30, 1948) is an American computer scientist and mathematician. He is the discoverer of several graph algorithms, including Tarjan's off-line lowest common ancestors algorithm, and co-inventor of both splay trees a ...

. He lived in

Juneau, Alaska The City and Borough of Juneau, more commonly known simply as Juneau ( ; tli, Dzánti K'ihéeni ), is the capital city of the state of Alaska. Located in the Gastineau Channel and the Alaskan panhandle, it is a unified municipality A mu ...

for a year before settling permanently in the

San Francisco Bay Area The San Francisco Bay Area, often referred to as simply the Bay Area, is a populous region surrounding the San Francisco, San Pablo, and Suisun Bay estuaries in Northern California. The Bay Area is defined by the Association of Bay Area Gov ...

Notable work

His thesis, ''Techniques for Program Verification'', influenced both

program verification In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal method ...

and

automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was ...

, especially in the area now named

satisfiability modulo theories In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involvin ...

, where he contributed techniques for combining decision procedures, as well as efficient decision procedures for quantifier-free constraints in

first-order logic First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quanti ...

and

term algebra In universal algebra and mathematical logic, a term algebra is a freely generated algebraic structure over a given signature. For example, in a signature consisting of a single binary operation, the term algebra over a set ''X'' of variables is exa ...

. He received the

Herbrand Award The Herbrand Award for Distinguished Contributions to Automated Reasoning is an award given by the Conference on Automated Deduction (CADE), Inc., (although it predates the formal incorporation of CADE) to honour persons or groups for important con ...

in 2013: He was instrumental in developing the ''Simplify'' theorem prover used by

ESC/Java ESC/Java (and more recently ESC/Java2), the "Extended Static Checker for Java," is a programming tool that attempts to find common run-time errors in Java programs at compile time. The underlying approach used in ESC/Java is referred to as exten ...

. He made significant contributions in several other areas. He contributed to the field of

programming language A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language. The description of a programming l ...

design as a member of the

Modula-3 Modula-3 is a programming language conceived as a successor to an upgraded version of Modula-2 known as Modula-2+. While it has been influential in research circles (influencing the designs of languages such as Java, C#, and Python) it has not ...

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 In computing, a windowing system (or window system) is software that manages separately different parts of display screens. It is a type of graphical user interface (GUI) which implements the WIMP (windows, icons, menus, pointer) paradigm for ...

(Trestle), optimal code generation (Denali), and multi- threaded programming (Eraser).

References

{{DEFAULTSORT:Nelson, Greg N. 1953 births 2015 deaths Harvard University alumni Stanford University School of Engineering alumni 20th-century American scientists 21st-century American scientists American computer scientists American computer programmers Programming language researchers Programming language designers Formal methods people Scientists from Hawaii Scientists at PARC (company)

Biography

Notable work

See also

References