Dexter Kozen

Joseph Newton Pew, Jr. Professor of Engineering
Ph.D. Cornell University, 1977

My research interests include the theory of computational complexity, especially complexity of decision problems in logic and algebra, program logic and semantics, and computational algebra. Recent work includes new polynomial-time algorithms for type inference in type systems with subtypes and recursive types; algorithms solving systems

of set constraints as used in program analysis; a unification algorithm for set constraints and a new constraint logic programming language based on set constraints; development of the theory of rational spaces and their relationship to set constraints; an algorithm for decomposition of algebraic functions; a new polynomial-time algorithm for resolution of singularities of plane curves; efficient algorithms for optimal transmission of encoded video data; optimality results for digital interleavers; and complexity and completeness results for Kleene algebras with tests. Recently I have begun to investigate algorithms for efficient code certification and the application of Kleene algebra with tests to the verification of compiler optimizations.


Class of 1960 Scholar, Williams College.

University Activities

Member: Undergraduate Admissions Committee, College of Engineering; University Arbitration Panel.

Faculty Advisor: Cornell Men’s Rugby Football Club; Johnson Graduate School of Management Rugby Football Club; Cornell Women’s Rugby Football Club.

Professional Activities

Program Committee Member: Foundations of Software Science and Computation Structure; Mathematical Foundations of Computer Science.

Editorial Board Member: Journal of Relational Methods in Computer Science; Journal of Algorithms (special issue).

Supervisory Board: Centre for Basic Research in Computer Science (BRICS), Aarhus University; Goedel Prize Committee.


Parikh’s Theorem in Commutative Kleene Algebra. FLOC ’99, Trento, Italy, July 1999.

On Hoare Logic and Kleene Algebra with Tests. FLOC ’99, Trento, Italy, July 1999. On Hoare Logic, Kleene Algebra, and Types. International Congress for Logic, Methodology and Philosophy of Science, Kracow, Poland, August 1999.

Language-based Security. 24th Conference on Mathematical Foundations of Computer Science, Wroclaw, Poland, September 1999.

—. Department of Computer Science, Dartmouth College, Hanover, NH, March 2000. On the completeness of propositional Hoare logic. RelMiCS 5 Conference, Quebec City, Canada, January 2000.


“Parikh’s theorem in commutative Kleene algebra.” Proc. Conference Logic in Computer Science (LICS ’99), 394–401, IEEE (July 1999) (with M. Hopkins).

“On Hoare Logic, Kleene Algebra, and Types.” Proc. Conference Logic in Computer Science (LICS ’99) IEEE (July 1999), 167–172.

“Language-based security.” Proc. Conference of Mathematical Foundations of Computer Science (MFCS ’99), volume 1672 of Lecture Notes in Computer Science, Springer-Verlag (September 1999), 284–298.

“Certification of Compiler Optimizations using Kleene Algebra with Tests.” In Proc. 1st Int. Conf. Computational Logic (CL2000), volume 1861 of Lecture Notes in Artificial Intelligence, J. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv, and P. J. Stuckey (Eds.), London, Springer-Verlag (July 2000), 568-582.

“On the completeness of propositional Hoare logic.” Proc. of the 5th International Seminar Relational Methods in Computer Science (RelMiCS 2000) (January 2000), 195–202 (with J. Tiuryn).

“Dynamic Logic.” MIT Press, Cambridge, MA (2000) (with D. Harel and J. Tiuryn).