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, CiteSeerX 10.1.1.368.3222 , 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 |
Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major motivating factor for the development of computer science.
Claude Elwood Shannon was an American mathematician, electrical engineer, computer scientist and cryptographer known as the "father of information theory" and as the "father of the Information Age". Shannon was the first to describe the Boolean gates that are essential to all digital electronic circuits, and was one of the founding fathers of artificial intelligence. 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 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 is the public engineering school of the University of California, Berkeley. Established in 1931, it occupies fourteen buildings on the northeast side of the main campus and also operates the 150-acre (61-hectare) Richmond Field Station. It is also considered highly selective and is consistently ranked among the top engineering schools in both the nation and the world.
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:
Reid William Barton is a mathematician and also one of the most successful performers in the International Science Olympiads.
Robert William Harper, Jr. is a computer science professor at Carnegie Mellon University who works in programming language research. Prior to his position at Carnegie Mellon, Harper was a research fellow at the University of Edinburgh.
The history of computer science began long before the modern discipline of computer science, usually appearing in forms like mathematics or physics. Developments in previous centuries alluded to the discipline that we now know as computer science. This progression, from mechanical inventions and mathematical theories towards modern computer concepts and machines, led to the development of a major academic field, massive technological advancement across the Western world, and the basis of a massive worldwide trade and culture.
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.
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 a full 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.
Emanuels Donats Frīdrihs Jānis Grinbergs was a Latvian mathematician, known for Grinberg's theorem on the Hamiltonicity of planar graphs.
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 introduce 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.