Dexter Kozen

Last updated

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.

Contents

Career

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 ]

Awards and honors

Related Research Articles

In mathematics, a Kleene algebra is an idempotent semiring endowed with a closure operator. It generalizes the operations known from regular expressions.

<span class="mw-page-title-main">Juris Hartmanis</span> American computer scientist (1928–2022)

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".

<span class="mw-page-title-main">Samson Abramsky</span> British computer scientist

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.

<span class="mw-page-title-main">Neil Immerman</span> American theoretical computer scientist

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.

<span class="mw-page-title-main">David Gries</span> American computer scientist

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•(aa)* ≤ 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.

<span class="mw-page-title-main">Yuri Gurevich</span> American computer scientist

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.

<span class="mw-page-title-main">Grigore Roșu</span> Computer science professor

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.

References

  1. Dexter Kozen at the Mathematics Genealogy Project
  2. "Dexter Kozen – Award Winner". Association for Computing Machinery . Retrieved 31 October 2013.
  3. "Professor Dexter Kozen". ru.nl. Retrieved 2015-03-17.[ dead link ]
  4. David Harel, Dexter Kozen, and Jerzy Tiuryn, "Dynamic Logic". MIT Press, 2000.
  5. Dexter Kozen (1983). "Results on the Propositional μ-Calculus". Theoretical Computer Science 27 (3): 333–354.
  6. Dexter Kozen (2006). Theory of Computation. Springer. ISBN   1-84628-297-7.
  7. "Cornell Rugby Football Club > Cornell Men Big Red Men > Team Contacts". Archived from the original on April 19, 2010. Retrieved October 7, 2010.
  8. 1 2 3 4 5 "Awards". Cornell Bowers CIS - Computer Science. Retrieved 2022-09-08.
  9. "Dexter C. Kozen". John Simon Guggenheim Memorial Foundation. Retrieved 2022-09-08.
  10. Kozen, Dexter; Tiuryn, Jerzy (1990). "Logics of programs". In van Leeuwen, Jan (ed.). Handbook of Theoretical Computer Science, volume B. Elsevier and MIT Press. pp. 789–840. ISBN   0444880747.
  11. Harel, David; Kozen, Dexter; Tiuryn, Jerzy (2000). Dynamic Logic. MIT Press. p. 476. ISBN   9780262527668.
  12. "AAAS Fellows" (PDF). AAAS . Retrieved 2022-09-08.
  13. Kozen, Dexter (1991). "A completeness theorem for Kleene algebras and the algebra of regular events". Proc. 1991 Sixth Annual IEEE Symp. on Logic in Computer Science. Amsterdam, Netherlands: IEEE Computer Society. pp. 214–225. doi:10.1109/LICS.1991.151646. hdl: 1813/6963 .
  14. "Weiss Presidential Fellow (for contributions to undergraduate education)". Cornell . Retrieved 2022-09-08.
  15. "POPL 2020 Program". SIGPLAN. Retrieved 2022-09-08.
  16. Smolka, Steffen; Foster, Nate; Hsu, Justin; Kappé, Tobias; Kozen, Dexter; Silva, Alexandra (January 2020). "Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time". Proc of the ACM on Programming Languages. Vol. 4. IEEE Computer Society. pp. 214–225. arXiv: 1907.05920 . doi: 10.1145/3371129 .
  17. "Alonzo Church Award". EACSL. Retrieved 2022-09-08.
  18. Kozen, Dexter (May 1977). "Kleene algebra with tests". ACM Transactions on Programming Languages and Systems . 19 (3): 427–443. doi: 10.1145/256167.256195 . S2CID   6658131.