Dexter Campbell Kozen (born December 20, 1951) is an American theoretical computer scientist. He is Joseph Newton Pew, Jr. Professor in Engineering at Cornell University.
Kozen received his B.A. from Dartmouth College in 1974 and his PhD in computer science in 1977 from Cornell University, where he was advised by Juris Hartmanis. [1]
He is a Fellow of the Association for Computing Machinery, [2] a Guggenheim Fellow, and has received an Outstanding Innovation Award from IBM Corporation. He has also been named Faculty of the Year by the Association of Computer Science Undergraduates at Cornell.
Kozen was one of the first professors to receive the honor of a professorship at The Radboud Excellence Initiative at Radboud University Nijmegen in the Netherlands. [3]
He is known for his work at the intersection of logic and complexity. He is one of the fathers of dynamic logic [4] and developed the version of the modal μ-calculus most used today. [5] Moreover, he has written several textbooks on the theory of computation, [6] automata theory, dynamic logic, and algorithms.
Kozen was a guitarist, singer, and songwriter in the band "Harmful if Swallowed". He also holds the position of faculty advisor for Cornell's rugby football club [7] and plays for the Cortland Homer Thundering Herd rugby team.[ citation needed ]
In mathematics, a Kleene algebra is an idempotent semiring endowed with a closure operator. It generalizes the operations known from regular expressions.
Juris Hartmanis was a Latvian-born American computer scientist and computational theorist who, with Richard E. Stearns, received the 1993 ACM Turing Award "in recognition of their seminal paper which established the foundations for the field of computational complexity theory".
Samson Abramsky is Professor of Computer Science at University College London. He was previously the Christopher Strachey Professor of Computing at Wolfson College, Oxford, from 2000 to 2021.
Neil Immerman is an American theoretical computer scientist, a professor of computer science at the University of Massachusetts Amherst. He is one of the key developers of descriptive complexity, an approach he is currently applying to research in model checking, database theory, and computational complexity theory.
Allan Bertram Borodin is a Canadian-American computer scientist who is a professor at the University of Toronto.
ACM SIGACT or SIGACT is the Association for Computing Machinery Special Interest Group on Algorithms and Computation Theory, whose purpose is support of research in theoretical computer science. It was founded in 1968 by Patrick C. Fischer.
In theoretical computer science, the modal μ-calculus is an extension of propositional modal logic by adding the least fixed point operator μ and the greatest fixed point operator ν, thus a fixed-point logic.
The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.
David Gries is an American computer scientist at Cornell University, mainly known for his books The Science of Programming (1981) and A Logical Approach to Discrete Math.
In algebraic logic, an action algebra is an algebraic structure which is both a residuated semilattice and a Kleene algebra. It adds the star or reflexive transitive closure operation of the latter to the former, while adding the left and right residuation or implication operations of the former to the latter. Unlike dynamic logic and other modal logics of programs, for which programs and propositions form two distinct sorts, action algebra combines the two into a single sort. It can be thought of as a variant of intuitionistic logic with star and with a noncommutative conjunction whose identity need not be the top element. Unlike Kleene algebras, action algebras form a variety, which furthermore is finitely axiomatizable, the crucial axiom being a•(a → a)* ≤ a. Unlike models of the equational theory of Kleene algebras (the regular expression equations), the star operation of action algebras is reflexive transitive closure in every model of the equations. Action algebras were introduced by Vaughan Pratt in the European Workshop JELIA'90.
Yuri Gurevich, Professor Emeritus at the University of Michigan, is an American computer scientist and mathematician and the inventor of abstract state machines.
Robert Lee Constable is an American computer scientist. He is a professor of computer science and first and former dean of the Faculty of Computing and Information Science at Cornell University. He is known for his work on connecting computer programs and mathematical proofs, especially the Nuprl system. Prior to Nuprl, he worked on the PL/CV formal system and verifier. Alonzo Church supervised Constable's junior thesis while he was studying in Princeton. Constable received his PhD in 1968 under Stephen Kleene and has supervised over 40 students.
Ronitt Rubinfeld is a professor of electrical engineering and computer science at the Massachusetts Institute of Technology (MIT) and the School of Computer Science at Tel Aviv University. At MIT she is a faculty lead for the Theory of Computation group at the Computer Science and Artificial Intelligence Laboratory.
Algorithmic logic is a calculus of programs that allows the expression of semantic properties of programs by appropriate logical formulas. It provides a framework that enables proving the formulas from the axioms of program constructs such as assignment, iteration and composition instructions and from the axioms of the data structures in question see Mirkowska & Salwicki (1987), Banachowski et al. (1977).
Henry A. Kautz is a computer scientist, Founding Director of Institute for Data Science and Professor at University of Rochester. He is interested in knowledge representation, artificial intelligence, data science and pervasive computing.
ACM SIGLOG or SIGLOG is the Association for Computing Machinery Special Interest Group on Logic and Computation. It publishes a news magazine, and has the annual ACM-IEEE Symposium on Logic in Computer Science (LICS) as its flagship conference. In addition, it publishes an online newsletter, the SIGLOG Monthly Bulletin, and "maintains close ties" with the related academic journal ACM Transactions on Computational Logic.
Phokion G. KolaitisACM is a computer scientist who is currently a Distinguished Research Professor at UC Santa Cruz and a Principal Research Staff Member at the IBM Almaden Research Center. His research interests include principles of database systems, logic in computer science, and computational complexity.
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.
Jin-Yi Cai is a Chinese American mathematician and computer scientist. He is a professor of computer science, and also the Steenbock Professor of Mathematical Sciences at the University of Wisconsin–Madison. His research is in theoretical computer science, especially computational complexity theory. In recent years he has concentrated on the classification of computational counting problems, especially counting graph homomorphisms, counting constraint satisfaction problems, and Holant problems as related to holographic algorithms.