About

Dexter Kozen is the Joseph Newton Pew, Jr. Professor Emeritus at Cornell University, having earned his PhD from Cornell in 1977. His research interests focus on the logics and semantics of programming languages, algorithms and complexity, with particular emphasis on the complexity of decision problems in logic and algebra, as well as probabilistic computation. Throughout his career, he has contributed to the theoretical foundations of computer science, especially in areas related to logic and computation. Kozen has also been involved in teaching a wide range of computer science courses at Cornell, spanning introductory computing, data structures, programming practicum, discrete structures, design and analysis of algorithms, theory of computing, logics of programs, and advanced programming languages. His work includes the development of interactive theorem provers and projects related to Kleene Algebra and natural deduction for first-order logic, reflecting his deep engagement with formal methods and computational logic.

Research topics

• Computer Science
• Artificial Intelligence
• Theoretical computer science
• Discrete mathematics
• Applied mathematics
• Programming language
• Pure mathematics
• Mathematics

Selected publications

• A Decision Procedure for Probabilistic Kleene Algebra with Angelic Nondeterminism

  ArXiv.org · 2025-07-15

  preprintOpen accessSenior author

  We give a decision procedure and proof of correctness for the equational theory of probabilistic Kleene algebra with angelic nondeterminism introduced in Ong, Ma, and Kozen (2025).

  PublisherOA PDFDOI

• 31st workshop on logic, language, information, and computation (<i>WoLLIC 2025</i>)

  Logic Journal of IGPL · 2025-08-15

  article1st authorCorresponding
  PublisherDOI

• A Demonic Outcome Logic for Randomized Nondeterminism

  Proceedings of the ACM on Programming Languages · 2025-01-07 · 4 citations

  articleOpen access

  Programs increasingly rely on randomization in applications such as cryptography and machine learning. Analyzing randomized programs has been a fruitful research direction, but there is a gap when programs also exploit nondeterminism(for concurrency, efficiency, or algorithmic design). In this paper, we introduce Demonic Outcome Logic for reasoning about programs that exploit both randomization and nondeterminism. The logic includes several novel features, such as reasoning about multiple executions in tandem and manipulating pre- and postconditions using familiar equational laws—including the distributive law of probabilistic choices over nondeterministic ones. We also give rules for loops that both establish termination and quantify the distribution of final outcomes from a single premise. We illustrate the reasoning capabilities of Demonic Outcome Logic through several case studies, including the Monty Hall problem, an adversarial protocol for simulating fair coins, and a heuristic based probabilistic SAT solver.

  PublisherDOI

• Probabilistic Kleene Algebra with Angelic Nondeterminism

  Proceedings of the ACM on Programming Languages · 2025-06-10

  preprintOpen accessSenior author

  We introduce a version of probabilistic Kleene algebra with angelic nondeterminism and a corresponding class of automata. Our approach implements semantics via distributions over multisets in order to overcome theoretical barriers arising from the lack of a distributive law between the powerset and Giry monads. We produce a full Kleene theorem and a coalgebraic theory, as well as both operational and denotational semantics and equational reasoning principles.

  PublisherDOI

• StacKAT: Infinite State Network Verification

  Proceedings of the ACM on Programming Languages · 2025-06-10

  articleOpen access

  We develop StacKAT, a network verification language featuring loops, finite state variables, nondeterminism, and---most importantly---access to a stack with accompanying push and pop operations. By viewing the variables and stack as the (parsed) headers and (to-be-parsed) contents of a network packet, StacKAT can express a wide range of network behaviors including parsing, source routing, and telemetry. These behaviors are difficult or impossible to model using existing languages like NetKAT. We develop a decision procedure for StacKAT program equivalence, based on finite automata. This decision procedure provides the theoretical basis for verifying network-wide properties and is able to provide counterexamples for inequivalent programs. Finally, we provide an axiomatization of StacKAT equivalence and establish its completeness.

  PublisherDOI

• A Cyclic Proof System for Guarded Kleene Algebra with Tests

  Lecture notes in computer science · 2024-01-01 · 2 citations

  book-chapterOpen access

  Abstract Guarded Kleene Algebra with Tests ( $$\texttt{GKAT}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>GKAT</mml:mi> </mml:math> for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about simple imperative while-programs. Following earlier work by Das and Pous on Kleene Algebra, we study $$\texttt{GKAT}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>GKAT</mml:mi> </mml:math> from a proof-theoretical perspective. The deterministic nature of $$\texttt{GKAT}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>GKAT</mml:mi> </mml:math> allows for a non-well-founded sequent system whose set of regular proofs is complete with respect to the guarded language model. This is unlike the situation with Kleene Algebra, where hypersequents are required. Moreover, the decision procedure induced by proof search runs in $$\textsf{NLOGSPACE}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>NLOGSPACE</mml:mi> </mml:math> , whereas that of Kleene Algebra is in $$\textsf{PSPACE}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>PSPACE</mml:mi> </mml:math> .

  PublisherOA PDFDOI

• Multisets and Distributions

  Lecture notes in computer science · 2024-01-01 · 2 citations

  book-chapter1st authorCorresponding
  PublisherDOI

• A cyclic proof system for Guarded Kleene Algebra with Tests (full version)

  arXiv (Cornell University) · 2024-05-13

  preprintOpen access

  Guarded Kleene Algebra with Tests (GKAT for short) is an efficient fragment of Kleene Algebra with Tests, suitable for reasoning about simple imperative while-programs. Following earlier work by Das and Pous on Kleene Algebra, we study GKAT from a proof-theoretical perspective. The deterministic nature of GKAT allows for a non-well-founded sequent system whose set of regular proofs is complete with respect to the guarded language model. This is unlike the situation with Kleene Algebra, where hypersequents are required. Moreover, the decision procedure induced by proof search runs in NLOGSPACE, whereas that of Kleene Algebra is in PSPACE.

  PublisherOA PDFDOI

• Formal Abstractions for Packet Scheduling

  Proceedings of the ACM on Programming Languages · 2023-10-16 · 7 citations

  articleOpen accessSenior author

  Early programming models for software-defined networking (SDN) focused on basic features for controlling network-wide forwarding paths, but more recent work has considered richer features, such as packet scheduling and queueing, that affect performance. In particular, PIFO trees , proposed by Sivaraman et al., offer a flexible and efficient primitive for programmable packet scheduling. Prior work has shown that PIFO trees can express a wide range of practical algorithms including strict priority, weighted fair queueing, and hierarchical schemes. However, the semantic properties of PIFO trees are not well understood. This paper studies PIFO trees from a programming language perspective. We formalize the syntax and semantics of PIFO trees in an operational model that decouples the scheduling policy running on a tree from the topology of the tree. Building on this formalization, we develop compilation algorithms that allow the behavior of a PIFO tree written against one topology to be realized using a tree with a different topology. Such a compiler could be used to optimize an implementation of PIFO trees, or realize a logical PIFO tree on a target with a fixed topology baked into the hardware. To support experimentation, we develop a software simulator for PIFO trees, and we present case studies illustrating its behavior on standard and custom algorithms.

  PublisherOA PDFDOI

• Minimisation in Logical Form

  Outstanding contributions to logic · 2023 · 6 citations

  • Computer Science
  • Mathematics
  • Pure mathematics
  PublisherOA PDFDOI

Recent grants

• SHF: Small: Semantics of Higher Order Probabilistic Programs

  NSF · $425k · 2020–2023

• Specialized Logics for Applications in Computer Science

  NSF · $250k · 2006–2010

Frequent coauthors

• Alexandra Silva

  Cornell University

  44 shared

• Juris Hartmanis

  Lancaster University

  34 shared

• W Brauer

  Institute of Informatics of the Slovak Academy of Sciences

  33 shared

• Krzysztof R. Apt

  Centrum Wiskunde & Informatica

  30 shared

• P. van Emde Boas

  29 shared

• R. M. Burstall

  29 shared

• Marek Karpiński

  Adam Mickiewicz University in Poznań

  26 shared

• László Lovász

  Alfréd Rényi Institute of Mathematics

  25 shared

Labs

• Dexter Kozen's LabPI

  Research interests: Logics and semantics of programming languages, algorithms and complexity, especially complexity of decision problems in logic and algebra, probabilistic computation.

Education

• PhD, Computer Science

  Cornell University

  1977

• BA, Mathematics

  Dartmouth College

  1974

Awards & honors

• Guggenheim Fellowship
• John G. Kemeny Prize in Computing
• IBM Outstanding Innovation Award
• EATCS Award
• IEEE W. Wallace McDowell Award