James Benjamin Saxe is an American computer scientist who has worked for many years at the DEC Systems Research Center [1] and its successors, the Compaq Systems Research Center and the Systems Research Center of HP Labs.
Saxe is known for his highly-cited publications on automated theorem proving, [DNS] circuit complexity, [FSS] retiming in synchronous circuit design, [LS] computer networks, [AOS] and static program analysis. [FLL] His work on program analysis from PLDI 2002 won the Most Influential PLDI Paper Award for 2012. [2] In addition, he is one of the authors of the master theorem for divide-and-conquer recurrences. [BHS]
While a high school student, Saxe won the United States of America Mathematical Olympiad. [3] In 1974, as a student at Union College, Saxe took part in the William Lowell Putnam Mathematical Competition; his place in the top five scores earned him a Putnam Fellowship. [4] He graduated from Union College in 1976, [3] , and earned his Ph.D. in 1985 from Carnegie Mellon University, under the supervision of Jon Bentley. [5]
BHS. | Bentley, Jon Louis; Haken, Dorothea; Saxe, James B. (September 1980), "A general method for solving divide-and-conquer recurrences", ACM SIGACT News , 12 (3): 36–44, doi:10.1145/1008861.1008865, S2CID 40642274 |
FSS. | Furst, Merrick; Saxe, James B.; Sipser, Michael (1984), "Parity, circuits, and the polynomial-time hierarchy", Mathematical Systems Theory, 17 (1): 13–27, doi:10.1007/BF01744431, MR 0738749, S2CID 14677270 |
LS. | Leiserson, Charles E.; Saxe, James B. (1991), "Retiming synchronous circuitry", Algorithmica , 6 (1): 5–35, doi:10.1007/BF01759032, MR 1079368, S2CID 18674287 |
AOS. | Anderson, Thomas E.; Owicki, Susan S.; Saxe, James B.; Thacker, Charles P. (November 1993), "High-speed switch scheduling for local-area networks", ACM Transactions on Computer Systems , 11 (4): 319–352, doi: 10.1145/161541.161736 , S2CID 53244607 |
FLL. | Flanagan, Cormac; Leino, K. Rustan M.; Lillibridge, Mark; Nelson, Greg; Saxe, James B.; Stata, Raymie (May 2002), "Extended static checking for Java", Proceedings of PLDI 2002, SIGPLAN Notices, 37 (5): 234–245, doi:10.1145/543552.512558 |
DNS. | Detlefs, David; Nelson, Greg; Saxe, James B. (2005), "Simplify: a theorem prover for program checking", Journal of the ACM , 52 (3): 365–473, doi:10.1145/1066100.1066102, MR 2146512, S2CID 9613854 |
Claude Elwood Shannon was an American mathematician, electrical engineer, computer scientist and cryptographer known as the "father of information theory". He is credited alongside George Boole for laying the foundations of the Information Age.
A computer algebra system (CAS) or symbolic algebra system (SAS) is any mathematical software with the ability to manipulate mathematical expressions in a way similar to the traditional manual computations of mathematicians and scientists. The development of the computer algebra systems in the second half of the 20th century is part of the discipline of "computer algebra" or "symbolic computation", which has spurred work in algorithms over mathematical objects such as polynomials.
Daniel Julius Bernstein is an American German mathematician, cryptologist, and computer scientist. He is a visiting professor at CASA at Ruhr University Bochum, as well as a research professor of Computer Science at the University of Illinois at Chicago. Before this, he was a visiting professor in the department of mathematics and computer science at the Eindhoven University of Technology.
The University of California, Berkeley College of Engineering, branded as Berkeley Engineering, is the engineering school of the University of California, Berkeley, a public research university in Berkeley, California.
Logic in computer science covers the overlap between the field of logic and that of computer science. The topic can essentially be divided into three main areas:
Michael Fredric Sipser is an American theoretical computer scientist who has made early contributions to computational complexity theory. He is a professor of applied mathematics and was the Dean of Science at the Massachusetts Institute of Technology.
Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is closely related to other fields including mathematics, software engineering, and linguistics. There are a number of academic conferences and journals in the area.
Andrew Mattei Gleason (1921–2008) was an American mathematician who made fundamental contributions to widely varied areas of mathematics, including the solution of Hilbert's fifth problem, and was a leader in reform and innovation in mathematics teaching at all levels. Gleason's theorem in quantum logic and the Greenwood–Gleason graph, an important example in Ramsey theory, are named for him.
Monica Sin-Ling Lam is an American computer scientist. She is a professor in the Computer Science Department at Stanford University.
Daniel Mertz Kane is an American mathematician. He is an associate professor with a joint position in the Mathematics Department and the Computer Science and Engineering Department at the University of California, San Diego.
Henry Otto Pollak is an Austrian-American mathematician. He is known for his contributions to information theory, and with Ronald Graham is the namesake of the Graham–Pollak theorem in graph theory.
Sung-Mo “Steve” Kang is an American electrical engineering scientist, professor, writer, inventor, entrepreneur and 15th president of KAIST. Kang was appointed as the second chancellor of the University of California, Merced in 2007. He was the first department head of foreign origin at the electrical and computer engineering department at the University of Illinois at Urbana-Champaign. Kang teaches and has written extensively in the field of computer-aided design for electronic circuits and systems; he is recognized and respected worldwide for his outstanding research contributions. Kang has led the development of the world’s first 32-bit microprocessor chips as a technical supervisor at AT&T Bell Laboratories and designed satellite-based private communication networks as a member of technical staff. Kang holds 15 U.S. patents and has won numerous awards for his ground breaking achievements in the field of electrical engineering.
Emanuels Donats Frīdrihs Jānis Grinbergs was a Latvian mathematician, known for Grinberg's theorem on the Hamiltonicity of planar graphs.
Michael Lin is an Israeli mathematician, who has published scientific articles in the field of probability concentrating on Markov chains and ergodic theory. He serves as professor emeritus at the Department of Mathematics in Ben-Gurion University of the Negev (BGU). Additionally, he is a member of the academic board and serves as the academic coordinator at Achva Academic College. Professor Lin is considered a Zionist, as he gave up a position at Ohio State University in order to promote the field of mathematics in Israel.
Thomas W. Reps is an American computer scientist known for his contributions to automatic program analysis. Dr. Reps is Professor of Computer Science in the Computer Sciences Department of the University of Wisconsin–Madison, which he joined in 1985. Reps is the author or co-author of four books and more than one hundred seventy-five papers describing his research. His work has covered a wide variety of topics, including program slicing, data-flow analysis, pointer analysis, model checking, computer security, instrumentation, language-based program-development environments, the use of program profiling in software testing, software renovation, incremental algorithms, and attribute grammars.
Kathleen Shanahan Fisher is an American computer scientist who specializes in programming languages and their implementation.
Mooly (Shmuel) Sagiv is an Israeli computer scientist known for his work on static program analysis. He is currently Chair of Software Systems in the School of Computer Science at Tel Aviv University, and CEO of Certora, a startup company providing formal verification of smart contracts.
Grigore Roșu is a computer science professor at the University of Illinois at Urbana-Champaign and a researcher in the Information Trust Institute. He is known for his contributions in runtime verification, the K framework, matching logic, and automated coinduction.
Ilya Sergey is a Russian computer scientist and an Associate Professor at the School of Computing at the National University of Singapore, where he leads the Verified Systems Engineering lab. Sergey does research in programming language design and implementation, software verification, distributed systems, program synthesis, and program repair. He is known for designing the Scilla programming language for smart contracts. He is the author of the free online book, Programs and Proofs: Mechanizing Mathematics with Dependent Types, Lecture notes with exercises, which provides an introduction to the basic concepts of mechanized reasoning and interactive theorem proving using Coq.
Todd Millstein is an American computer scientist. He is Professor of Computer Science and Chair of the Department at the UCLA Henry Samueli School of Engineering and Applied Science.