Publications — Dexter Kozen

[Kleene Algebra & Logic] [Programming Languages & Program Analysis] [Computational Algebra] [Automata & Formal Languages] [Algorithms & Complexity] [Coding Theory] [Security] [Other]

[By year] [Home]

---

Kleene Algebra & Logic

• Noam Zilberstein, Dexter Kozen, Alexandra Silva, and Joseph Tassarotti. A demonic outcome logic for randomized nondeterminism. Technical Report https://arxiv.org/abs/2410.22540, Cornell University, October 2024. POPL 2025, to appear.
  [full text] [abstract] [bibtex] []

  @techreport{ZKSTa24,
    author="Noam Zilberstein and Dexter Kozen and Alexandra Silva and Joseph Tassarotti",
    title="A Demonic Outcome Logic for Randomized Nondeterminism",
    month="October",
    year="2024",
    institution="Cornell University",
    number="{\url{https://arxiv.org/abs/2410.22540}}",
    note="POPL 2025, to appear"
  }

  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.

• Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva. Probabilistic guarded KAT modulo bisimilarity: Completeness and complexity. In Kousha Etessami, Uriel Feige, and Gabriele Puppis, editors, Proc. 50th Int. Colloq. on Automata, Languages, and Programming (ICALP'23), volume 261 of Leibniz International Proceedings in Informatics (LIPIcs), pages 136:1-136:20, Paderborn, Germany, July 2023. (Extended version: Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva. Probabilistic guarded KAT modulo bisimilarity: Completeness and complexity. Technical Report https://arxiv.org/abs/2305.01755, Cornell University, May 2023.)
  [full text] [abstract] [bibtex] []

  @inproceedings{RKKSS23b,
    author="Wojciech R\'{o}żowski and Tobias Kapp{\'e} and Dexter Kozen and Todd Schmid and Alexandra Silva",
    title="Probabilistic Guarded {KAT} Modulo Bisimilarity: Completeness and Complexity",
    booktitle="Proc. 50th Int. Colloq. on Automata, Languages, and Programming (ICALP'23)",
    series="Leibniz International Proceedings in Informatics (LIPIcs)",
    editor="Etessami, Kousha and Feige, Uriel and Puppis, Gabriele",
    volume="261",
    address="Paderborn, Germany",
    month="July",
    year="2023",
    pages="136:1--136:20"
  }

  We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimilarity of ProbGKAT expressions can be decided in $O(n^3 \log n)$ time via a generic partition refinement algorithm.

• Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva. Probabilistic guarded KAT modulo bisimilarity: Completeness and complexity. Technical Report https://arxiv.org/abs/2305.01755, Cornell University, May 2023. (Extended version of: Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid, and Alexandra Silva. Probabilistic guarded KAT modulo bisimilarity: Completeness and complexity. In Kousha Etessami, Uriel Feige, and Gabriele Puppis, editors, Proc. 50th Int. Colloq. on Automata, Languages, and Programming (ICALP'23), volume 261 of Leibniz International Proceedings in Informatics (LIPIcs), pages 136:1-136:20, Paderborn, Germany, July 2023.)
  [full text] [abstract] [bibtex] []

  @techreport{RKKSS23a,
    author="Wojciech R\'{o}żowski and Tobias Kapp{\'e} and Dexter Kozen and Todd Schmid and Alexandra Silva",
    title="Probabilistic Guarded {KAT} Modulo Bisimilarity: Completeness and Complexity",
    month="May",
    year="2023",
    institution="Cornell University",
    number="{\url{https://arxiv.org/abs/2305.01755}}"
  }

  We introduce Probabilistic Guarded Kleene Algebra with Tests (ProbGKAT), an extension of GKAT that allows reasoning about uninterpreted imperative programs with probabilistic branching. We give its operational semantics in terms of special class of probabilistic automata. We give a sound and complete Salomaa-style axiomatisation of bisimilarity of ProbGKAT expressions. Finally, we show that bisimilarity of ProbGKAT expressions can be decided in $O(n^3 \log n)$ time via a generic partition refinement algorithm.

• Jana Wagemaker, Nate Foster, Tobias Kappé, Dexter Kozen, Jurriaan Rot, and Alexandra Silva. Concurrent NetKAT: Modeling and analyzing stateful, concurrent networks. In 31st European Symposium on Programming (ESOP'22), April 2022.
  [full text] [abstract] [bibtex] []

  @inproceedings{WFKKRSa,
    author="Jana Wagemaker and Nate Foster and Tobias Kapp\'e and Dexter Kozen and Jurriaan Rot and Alexandra Silva",
    title="Concurrent {NetKAT}: Modeling and analyzing stateful, concurrent networks",
    booktitle="31st European Symposium on Programming (ESOP'22)",
    month="April",
    year="2022"
  }

  We introduce Concurrent NetKAT (CNetKAT), an extension of the network programming language NetKAT with multiple packets and with operators to specify and reason about concurrency and state. We provide a model of the language based on partially ordered multisets (pomsets), well-established mathematical structures in the denotational semantics of concurrent languages. We prove that CNetKAT is a sound and complete axiomatization of this model, and we illustrate the use of CNetKAT through various examples. More generally, CNetKAT is an algebraic framework to reason about programs with both local and global state. In our model these are, respectively, the packets and the global variable store, but the scope of applications is much more general, including reasoning about hardware pipelines inside an SDN switch.

• Todd Schmid, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: Coequations, coinduction, and completeness. In Int. Colloq. Automata, Languages and Programming (ICALP'21). EATCS, July 2021.
  [full text] [abstract] [bibtex] []

  @inproceedings{SKKS21a,
    author="Todd Schmid and Tobias Kappé and Dexter Kozen and Alexandra Silva",
    title="Guarded {K}leene Algebra with Tests: {C}oequations, Coinduction, and Completeness",
    booktitle="Int. Colloq. Automata, Languages and Programming (ICALP'21)",
    organization="EATCS",
    month="July",
    year="2021"
  }

  Guarded Kleene Algebra with Tests (GKAT) is an efficient fragment of KAT, as it allows for almost linear decidability of equivalence. In this paper, we study the (co)algebraic properties of GKAT. Our initial focus is on the fragment that can distinguish between unsuccessful programs performing different actions, by omitting the so-called early termination axiom. We develop an operational (coalgebraic) and denotational (algebraic) semantics and show that they coincide. We then characterize the behaviors of GKAT expressions in this semantics, leading to a coequation that captures the covariety of automata corresponding to behaviors of GKAT expressions. Finally, we prove that the axioms of the reduced fragment are sound and complete w.r.t. the semantics, and then build on this result to recover a semantics that is sound and complete w.r.t. the full set of axioms.

• Nick Bezhanishvili, Marcello Bonsangue, Helle Hvid Hansen, Dexter Kozen, Clemens Kupke, Prakash Panangaden, and Alexandra Silva. Minimisation in logical form. Technical Report http://arxiv.org/abs/2005.11551, Cornell University, May 2020.
  [full text] [abstract] [bibtex] []

  @techreport{bezhanishvili2020minimisation,
    author="Nick Bezhanishvili and Marcello Bonsangue and Helle Hvid Hansen and Dexter Kozen and Clemens Kupke and Prakash Panangaden and Alexandra Silva",
    title="Minimisation in Logical Form",
    month="May",
    year="2020",
    institution="Cornell University",
    number="{\url{http://arxiv.org/abs/2005.11551}}"
  }

  Stone-type dualities provide a powerful mathematical framework for studying properties of logical systems. They have recently been fruitfully explored in understanding minimisation of various types of automata. In Bezhanishvili et al. (2012), a dual equivalence between a category of coalgebras and a category of algebras was used to explain minimisation. The algebraic semantics is dual to a coalgebraic semantics in which logical equivalence coincides with trace equivalence. It follows that maximal quotients of coalgebras correspond to minimal subobjects of algebras. Examples include partially observable deterministic finite automata, linear weighted automata viewed as coalgebras over finite-dimensional vector spaces, and belief automata, which are coalgebras on compact Hausdorff spaces. In Bonchi et al. (2014), Brzozowski's double-reversal minimisation algorithm for deterministic finite automata was described categorically and its correctness explained via the duality between reachability and observability. This work includes generalisations of Brzozowski's algorithm to Moore and weighted automata over commutative semirings. In this paper we propose a general categorical framework within which such minimisation algorithms can be understood. The goal is to provide a unifying perspective based on duality. Our framework consists of a stack of three interconnected adjunctions: a base dual adjunction that can be lifted to a dual adjunction between coalgebras and algebras and also to a dual adjunction between automata. The approach provides an abstract understanding of reachability and observability. We illustrate the general framework on range of concrete examples, including deterministic Kripke frames, weighted automata, topological automata (belief automata), and alternating automata.

• Dexter Kozen and Alexandra Silva. Left-handed completeness. Theoretical Computer Science, 807:220-233, 6 February 2020. URL: http://www.sciencedirect.com/science/article/pii/S0304397519306838, doi:10.1016/j.tcs.2019.10.040.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KS20a,
    author="Dexter Kozen and Alexandra Silva",
    title="Left-Handed Completeness",
    journal="Theoretical Computer Science",
    volume="807",
    month="6 February",
    year="2020",
    pages="220--233",
    doi="10.1016/j.tcs.2019.10.040",
    url="{http://www.sciencedirect.com/science/article/pii/S0304397519306838}"
  }

  We give a new proof of the completeness of the left-handed star rule of Kleene algebra. The proof is significantly shorter than previous proofs and exposes the rich interaction of algebra and coalgebra in the theory of Kleene algebra.

• Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: Verification of uninterpreted programs in nearly linear time. In Proc. 47th ACM SIGPLAN Symp. Principles of Programming Languages (POPL'20), pages 61:1-28, New Orleans, January 2020. ACM. (Extended version: Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: Verification of uninterpreted programs in nearly linear time. Technical Report http://arxiv.org/abs/1907.05920, Cornell University, July 2019.)
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{SFHKKS20a,
    author="Steffen Smolka and Nate Foster and Justin Hsu and Tobias Kapp\'e and Dexter Kozen and Alexandra Silva",
    title="Guarded {K}leene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time",
    booktitle="Proc. 47th ACM SIGPLAN Symp. Principles of Programming Languages (POPL'20)",
    organization="ACM",
    pages="61:1--28",
    address="New Orleans",
    month="January",
    year="2020"
  }

  Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union ($+$) and iteration ($*$) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa's axiomatization of Kleene Algebra.

• Zoltán Ésik and Dexter Kozen. On free ω-continuous and regular ordered algebras. Logical Methods in Computer Science, 15(4):1-16, October 2019. URL: https://lmcs.episciences.org/5876.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{EK19,
    author="Zolt{\'a}n {\'E}sik and Dexter Kozen",
    title="On Free $\omega$-Continuous and Regular Ordered Algebras",
    journal="Logical Methods in Computer Science",
    volume="15",
    number="4",
    month="October",
    year="2019",
    pages="1--16",
    url="{https://lmcs.episciences.org/5876}"
  }

  We study varieties of certain ordered $\Sigma$-algebras with restricted completeness and continuity properties. We give a general characterization of their free algebras in terms of submonads of the monad of $\Sigma$-coterms. Varieties of this form are called quasi-regular. For example, we show that if $E$ is a set of inequalities between finite $\Sigma$-terms, and if ${\mathcal{V}}_\omega$ and ${\mathcal{V}}_{\mathrm{reg}}$ denote the varieties of all $\omega$-continuous ordered $\Sigma$-algebras and regular ordered $\Sigma$-algebras satisfying $E$, respectively, then the free ${\mathcal{V}}_{\mathrm{reg}}$-algebra $F_{\mathrm{reg}}(X)$ on generators $X$ is the subalgebra of the corresponding free ${\mathcal{V}}_\omega$-algebra $F_\omega(X)$ determined by those elements of $F_\omega(X)$ denoted by the regular $\Sigma$-coterms. This is a special case of a more general construction that applies to any quasi-regular family. Examples include the *-continuous Kleene algebras, context-free languages, $\omega$-continuous semirings and $\omega$-continuous idempotent semirings, OI-macro languages, and iteration theories.

• Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: Verification of uninterpreted programs in nearly linear time. Technical Report http://arxiv.org/abs/1907.05920, Cornell University, July 2019. (Extended version of: Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: Verification of uninterpreted programs in nearly linear time. In Proc. 47th ACM SIGPLAN Symp. Principles of Programming Languages (POPL'20), pages 61:1-28, New Orleans, January 2020. ACM.)
  [full text] [abstract] [bibtex] []

  @techreport{SFHKKS19a,
    author="Steffen Smolka and Nate Foster and Justin Hsu and Tobias Kapp\'e and Dexter Kozen and Alexandra Silva",
    title="Guarded {K}leene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time",
    institution="Cornell University",
    number="{\url{http://arxiv.org/abs/1907.05920}}",
    month="July",
    year="2019"
  }

  Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union ($+$) and iteration ($*$) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa's axiomatization of Kleene Algebra.

• Dexter Kozen and Matvey Soloviev. Coalgebraic tools for randomness-conserving protocols. In J. Desharnais, W. Guttmann, and S. Joosten, editors, Relational and Algebraic Methods in Computer Science (RAMiCS 2018), volume 11194 of LNCS, pages 298-313. Springer, October 2018. (Subsumed by Dexter Kozen and Matvey Soloviev. Coalgebraic tools for randomness-conserving protocols. J. Logical and Algebraic Methods in Programming, 125:100734, February 2022. doi:10.1016/j.jlamp.2021.100734.)
  [full text] [abstract] [bibtex] []

  @inproceedings{KS18a,
    author="Dexter Kozen and Matvey Soloviev",
    title="Coalgebraic Tools for Randomness-Conserving Protocols",
    booktitle="Relational and Algebraic Methods in Computer Science (RAMiCS 2018)",
    city="Groningen, The Netherlands",
    publisher="Springer",
    series="LNCS",
    volume="11194",
    editor="J. Desharnais and W. Guttmann and S. Joosten",
    month="October",
    year="2018",
    pages="298--313"
  }

  We propose a coalgebraic model for constructing and reasoning about state-based protocols that implement efficient reductions among random processes. We provide basic tools that allow efficient protocols to be constructed in a compositional way and analyzed in terms of the tradeoff between latency and loss of entropy. We show how to use these tools to construct various entropy-conserving reductions between processes.

• Giorgio Bacci, Robert Furber, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Dana Scott. Boolean-valued semantics for the stochastic λ-calculus. In Proc. 33rd Conf. Logic in Computer Science (LICS 2018), Oxford, UK, July 2018. ACM SIGLOG and IEEE.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{BFKMPS18a,
    author="Giorgio Bacci and Robert Furber and Dexter Kozen and Radu Mardare and Prakash Panangaden and Dana Scott",
    title="Boolean-Valued Semantics for the Stochastic $\lambda$-Calculus",
    booktitle="Proc. 33rd Conf. Logic in Computer Science (LICS 2018)",
    publisher="ACM SIGLOG and IEEE",
    address="Oxford, UK",
    month="July",
    year="2018"
  }

  The ordinary untyped $\lambda$-calculus has a set-theoretic model proposed in two related forms by Scott and Plotkin in the 1970s. Recently Scott showed how to introduce probability by extending these models with random variables. However, to reason about correctness and to add further features, it is useful to reinterpret the construction in a higher-order Boolean-valued model involving a measure algebra. In this paper we develop the semantics of an extended stochastic $\lambda$-calculus suitable for modeling a simple higher-order probabilistic programming language. We exhibit a number of key equations satisfied by the terms of our language. The terms are interpreted using a continuation-style semantics with an additional argument, an infinite sequence of coin tosses, which serve as a source of randomness. The construction of the model requires a subtle measure-theoretic analysis of the space of coin-tossing sequences. We also introduce a fixpoint operator as a new syntactic construct, as $\beta$-reduction turns out not to be sound for unrestricted terms. Finally, we develop a new notion of equality between terms interpreted in a measure algebra, allowing one to reason about terms that may not be equal almost everywhere. This provides a new framework and reasoning principles for probabilistic programs and their higher-order properties.

• Dexter Kozen, Konstantinos Mamouras, and Alexandra Silva. Completeness and incompleteness in nominal Kleene algebra. J. Logical and Algebraic Methods in Programming, 91:17-32, 2017. doi:10.1016/j.jlamp.2017.06.002.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KMS17a,
    author="Dexter Kozen and Konstantinos Mamouras and Alexandra Silva",
    title="Completeness and Incompleteness in Nominal {K}leene Algebra",
    journal="J. Logical and Algebraic Methods in Programming",
    volume="91",
    pages="17--32",
    doi="10.1016/j.jlamp.2017.06.002",
    year="2017"
  }

  Gabbay and Ciancia (2011) presented a nominal extension of Kleene algebra as a framework for trace semantics with dynamic allocation of resources, along with a semantics consisting of nominal languages. They also provided an axiomatization that captures the behavior of the scoping operator and its interaction with the Kleene algebra operators and proved soundness over nominal languages. In this paper we show that the axioms are complete and describe the free language models.

• Robert Furber, Dexter Kozen, Kim Larsen, Radu Mardare, and Prakash Panangaden. Unrestricted Stone duality for Markov processes. In Proc. 32nd Conf. Logic in Computer Science (LICS 2017). ACM SIGLOG and IEEE, June 2017.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{FKLMP17a,
    author="Robert Furber and Dexter Kozen and Kim Larsen and Radu Mardare and Prakash Panangaden",
    title="Unrestricted {S}tone Duality for {M}arkov Processes",
    booktitle="Proc. 32nd Conf. Logic in Computer Science (LICS 2017)",
    organization="ACM SIGLOG and IEEE",
    city="Reykjavik, Iceland",
    month="June",
    year="2017"
  }

  Stone duality relates logic, in the form of Boolean algebra, to spaces. Stone-type dualities abound in computer science and have been of great use in understanding the relationship between computational models and the languages used to reason about them. Recent work on probabilistic processes has established a Stone-type duality for a restricted class of Markov processes. The dual category was a new notion—Aumann algebras—which are Boolean algebras equipped with countable family of modalities indexed by rational probabilities. In this article we consider an alternative definition of Aumann algebra that leads to dual adjunction for Markov processes that is a duality for many measurable spaces occurring in practice. This extends a duality for measurable spaces due to Sikorski. In particular, we do not require that the probabilistic modalities preserve a distinguished base of clopen sets, nor that morphisms of Markov processes do so. The extra generality allows us to give a perspicuous definition of event bisimulation on Aumann algebras.

• Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann. Nominal automata with name binding. In J. Esparza and A. S. Murawski, editors, 20th Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS 2017), volume 10203 of Lecture Notes in Computer Science, pages 124-142. Springer, April 2017. doi:10.1007/978-3-662-54458-7_8.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KMSW17a,
    author="Lutz Schr{\"o}der and Dexter Kozen and Stefan Milius and Thorsten Wi{\ss}mann",
    title="Nominal Automata with Name Binding",
    booktitle="20th Int. Conf. Foundations of Software Science and Computation Structures (FOSSACS 2017)",
    editor="J. Esparza and A. S. Murawski",
    series="Lecture Notes in Computer Science",
    volume="10203",
    publisher="Springer",
    pages="124--142",
    doi="10.1007/978-3-662-54458-7_8",
    month="April",
    year="2017"
  }

  Nominal sets are a convenient setting for languages over infinite alphabets, i.e. data languages. We introduce an automaton model over nominal sets, regular nondeterministic nominal automata (RNNA), which have a natural coalgebraic definition using abstraction sets to capture transitions that read a fresh letter from the input word. We prove a Kleene theorem for RNNAs w.r.t. a simple expression language that extends nominal Kleene algebra (NKA) with unscoped name binding, thus remedying the known failure of the expected Kleene theorem for NKA itself. We analyse RNNAs under two notions of freshness: global and local. Under global freshness, RNNAs turn out to be equivalent to session automata, and as such have a decidable inclusion problem. Under local freshness, RNNAs retain a decidable inclusion problem, and translate into register automata. We thus obtain decidability of inclusion for a reasonably expressive class of nondeterministic register automata, with no bound on the number of registers.

• Dexter Kozen. On the coalgebraic theory of Kleene algebra with tests. In Can Başkent, Lawrence S. Moss, and Ramaswamy Ramanujam, editors, Rohit Parikh on Logic, Language and Society, volume 11 of Outstanding Contributions to Logic, pages 279-298. Springer, March 2017.
  [full text (.pdf)] [abstract] [bibtex] []

  @incollection{K17a,
    author="Dexter Kozen",
    title="On the Coalgebraic Theory of {K}leene Algebra with Tests",
    booktitle="Rohit Parikh on Logic, Language and Society",
    editor="Ba{\c{s}}kent, Can and Moss, Lawrence S. and Ramanujam, Ramaswamy",
    volume="11",
    series="Outstanding Contributions to Logic",
    month="March",
    year="2017",
    publisher="Springer",
    pages="279--298"
  }

  We develop a coalgebraic theory of Kleene algebra with tests (KAT) along the lines of Rutten (1998) for Kleene algebra (KA) and Chen and Pucella (2003) for a limited version of KAT, resolving some technical issues raised by Chen and Pucella. Our treatment includes a simple definition of the Brzozowski derivative for KAT expressions and an automata-theoretic interpretation involving automata on guarded strings. We also give a complexity analysis, showing that an efficient implementation of coinductive equivalence proofs in this setting is tantamount to a standard automata-theoretic construction. It follows that coinductive equivalence proofs can be generated automatically in PSPACE. This matches the bound of Worthington (2008) for the automatic generation of equational proofs in KAT.

• Niels Bjørn Bugge Grathwohl, Fritz Henglein, and Dexter Kozen. Infinitary axiomatization of the equational theory of context-free languages. Fundamenta Informaticae, 150:241-257, 2017. doi:10.3233/FI-2017-1469.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{GHK17a,
    author="Niels Bj{\o}rn Bugge Grathwohl and Fritz Henglein and Dexter Kozen",
    title="Infinitary Axiomatization of the Equational Theory of Context-Free Languages",
    journal="Fundamenta Informaticae",
    volume="150",
    year="2017",
    pages="241--257",
    doi="10.3233/FI-2017-1469"
  }

  We give a natural complete infinitary axiomatization of the equational theory of the context-free languages, answering a question of Leiss (1992).

• Dexter Kozen and Alexandra Silva. Practical coinduction. Mathematical Structures in Computer Science, 27:1132-1152, 2017. doi:10.1017/S0960129515000493.
  [journal link] [full text (.pdf)] [abstract] [bibtex] []

  @article{KS16a,
    author="Dexter Kozen and Alexandra Silva",
    title="Practical coinduction",
    journal="Mathematical Structures in Computer Science",
    volume="27",
    year="2017",
    pages="1132--1152",
    issn="1469-8072",
    doi="10.1017/S0960129515000493"
  }

  Induction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively defined datatypes such as finite lists, finite trees and the natural numbers. Coinduction is the dual principle that can be used to reason about coinductive datatypes such as infinite streams or trees, but it is not as widespread or as well understood. In this paper, we illustrate through several examples the use of coinduction in informal mathematical arguments. Our aim is to promote the principle as a useful tool for the working mathematician and to bring it to a level of familiarity on par with induction. We show that coinduction is not only about bisimilarity and equality of behaviors, but also applicable to a variety of functions and relations defined on coinductive datatypes.

• Dexter Kozen, Konstantinos Mamouras, Daniela Petrisan, and Alexandra Silva. Nominal Kleene coalgebra. In M. M. Halldórsson, K. Iwama, N. Kobayashi, and B. Speckmann, editors, Proc. 42nd Int. Colloq. Automata, Languages, and Programming, Part II (ICALP 2015), volume 9135 of Lecture Notes in Computer Science, pages 290-302, Kyoto, Japan, July 6-10 2015. EATCS, Springer.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KMPS15a,
    author="Dexter Kozen and Konstantinos Mamouras and Daniela Petrisan and Alexandra Silva",
    title="Nominal {K}leene Coalgebra",
    booktitle="Proc. 42nd Int. Colloq. Automata, Languages, and Programming, Part II (ICALP 2015)",
    organization="EATCS",
    pages="290--302",
    editor="M. M. Halld{\'o}rsson and K. Iwama and N. Kobayashi and B. Speckmann",
    publisher="Springer",
    series="Lecture Notes in Computer Science",
    volume="9135",
    address="Kyoto, Japan",
    month="July 6--10",
    year="2015"
  }

  We develop the coalgebraic theory of nominal Kleene algebra, including an alternative language-theoretic semantics, a nominal extension of the Brzozowski derivative, and a bisimulation-based decision procedure for the equational theory.

• Dexter Kozen, Konstantinos Mamouras, and Alexandra Silva. Completeness and incompleteness in nominal Kleene algebra. In Wolfram Kahl et al., editor, Relational and Algebraic Methods in Computer Science (RAMiCS 2015), volume 9348 of Lecture Notes in Computer Science, pages 51-66, Braga, Portugal, September 2015. Springer. (Subsumed by Dexter Kozen, Konstantinos Mamouras, and Alexandra Silva. Completeness and incompleteness in nominal Kleene algebra. J. Logical and Algebraic Methods in Programming, 91:17-32, 2017. doi:10.1016/j.jlamp.2017.06.002.)
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KMS15a,
    author="Dexter Kozen and Konstantinos Mamouras and Alexandra Silva",
    title="Completeness and Incompleteness in Nominal {K}leene Algebra",
    booktitle="Relational and Algebraic Methods in Computer Science (RAMiCS 2015)",
    pages="51--66",
    editor="Wolfram Kahl et al.",
    publisher="Springer",
    series="Lecture Notes in Computer Science",
    volume="9348",
    address="Braga, Portugal",
    month="September",
    year="2015"
  }

  Gabbay and Ciancia (2011) presented a nominal extension of Kleene algebra as a framework for trace semantics with dynamic allocation of resources, along with a semantics consisting of nominal languages. They also provided an axiomatization that captures the behavior of the scoping operator and its interaction with the Kleene algebra operators and proved soundness over nominal languages. In this paper we show that the axioms are complete and describe the free language models.

• Nate Foster, Dexter Kozen, Mae Milano, Alexandra Silva, and Laure Thompson. A coalgebraic decision procedure for NetKAT. In Proc. 42nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL'15), pages 343-355, Mumbai, India, January 2015. ACM.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{FKMST15a,
    author="Nate Foster and Dexter Kozen and Mae Milano and Alexandra Silva and Laure Thompson",
    title="A Coalgebraic Decision Procedure for {NetKAT}",
    booktitle="Proc. 42nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL'15)",
    organization="ACM",
    pages="343--355",
    address="Mumbai, India",
    month="January",
    year="2015"
  }

  Program equivalence is a fundamental problem that has practical applications across a variety of areas of computing including compilation, optimization, software synthesis, formal verification, and many others. Equivalence is undecidable in general, but in certain settings it is possible to develop domain-specific languages that are expressive enough to be practical and yet sufficiently restricted so that equivalence remains decidable. In previous work we introduced NetKAT, a domain-specific language for specifying and verifying network packet-processing functions. NetKAT provides familiar constructs such as tests, assignments, union, sequential composition, and iteration as well as custom primitives for modifying packet headers and encoding network topologies. Semantically, NetKAT is based on Kleene algebra with tests (KAT) and comes equipped with a sound and complete equational theory. Although NetKAT equivalence is decidable, the best known algorithm is hardly practical-it uses Savitch's theorem to determinize a PSPACE algorithm and requires quadratic space. This paper presents a new algorithm for deciding NetKAT equivalence. This algorithm is based on finding bisimulations between finite automata constructed from NetKAT programs. We investigate the coalgebraic theory of NetKAT, generalize the notion of Brzozowski derivatives to NetKAT, develop efficient representations of NetKAT automata in terms of spines and sparse matrices, and discuss the highlights of our prototype implementation.

• Dexter Kozen. NetKAT: A formal system for the verification of networks. In Jacques Garrigue, editor, Proc. 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), volume 8858 of Lecture Notes in Computer Science, Singapore, November 17-19 2014. Asian Association for Foundation of Software (AAFS), Springer.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{K14b,
    author="Dexter Kozen",
    title="{NetKAT}: A Formal System for the Verification of Networks",
    editor="Jacques Garrigue",
    booktitle="Proc. 12th Asian Symposium on Programming Languages and Systems (APLAS 2014)",
    organization="Asian Association for Foundation of Software (AAFS)",
    publisher="Springer",
    series="Lecture Notes in Computer Science",
    volume="8858",
    address="Singapore",
    month="November 17--19",
    year="2014"
  }

  This paper presents a survey of recent work in the development of NetKAT, a formal system for reasoning about packet switching networks, and its role in the emerging area of software-defined networking.

• Niels Bjørn Bugge Grathwohl, Dexter Kozen, and Konstantinos Mamouras. KAT + B! In Matthias Baaz, Thomas Eiter, and Helmut Veith, editors, Proc. Joint Meeting of the 23rd EACSL Conf. Computer Science Logic (CSL 2014) and 29th ACM/IEEE Symp. Logic in Computer Science (LICS 2014), Vienna, Austria, July 14-18 2014. EACSL and ACM/IEEE.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{GKM14a,
    author="Niels Bj{\o}rn Bugge Grathwohl and Dexter Kozen and Konstantinos Mamouras",
    title="{KAT + B!}",
    editor="Matthias Baaz and Thomas Eiter and Helmut Veith",
    booktitle="Proc. Joint Meeting of the 23rd EACSL Conf. Computer Science Logic (CSL 2014) and 29th ACM/IEEE Symp. Logic in Computer Science (LICS 2014)",
    organization="EACSL and ACM/IEEE",
    address="Vienna, Austria",
    month="July 14--18",
    year="2014"
  }

  It is known that certain program transformations require a small amount of mutable state, a feature not explicitly provided by Kleene algebra with tests (KAT). In this paper we show how to axiomatically extend KAT with this extra feature in the form of mutable tests. The extension is conservative and is formulated as a general commutative coproduct construction. We give several results on deductive completeness and complexity of the system, as well as some examples of its use.

• Dexter Kozen and Konstantinos Mamouras. Kleene algebra with equations. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, 41st Int. Colloq. Automata, Languages, and Programming (ICALP 2014), Part II, volume 8573 of Lecture Notes in Computer Science, pages 280-292, Copenhagen, Denmark, July 2014. EATCS, Springer.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KM14a,
    author="Dexter Kozen and Konstantinos Mamouras",
    title="Kleene Algebra with Equations",
    editor="Javier Esparza and Pierre Fraigniaud and Thore Husfeldt and Elias Koutsoupias",
    booktitle="41st Int. Colloq. Automata, Languages, and Programming (ICALP 2014), Part II",
    organization="EATCS",
    pages="280--292",
    address="Copenhagen, Denmark",
    publisher="Springer",
    series="Lecture Notes in Computer Science",
    volume="8573",
    month="July",
    year="2014"
  }

  We identify sufficient conditions for the construction of free language models for systems of Kleene algebra with additional equations. The construction applies to a broad class of extensions of KA and provides a uniform approach to deductive completeness and coalgebraic decision procedures.

• Dexter Kozen, Radu Mardare, and Prakash Panangaden. A metrized duality theorem for Markov processes. In Bart Jacobs, Alexandra Silva, and Sam Staton, editors, Proc. 30th Conf. Mathematical Foundations of Programming Semantics (MFPS'14), Electronic Notes in Theoretical Computer Science, pages 215-231. Elsevier, June 2014.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KMP14a,
    author="Dexter Kozen and Radu Mardare and Prakash Panangaden",
    title="A Metrized Duality Theorem for {M}arkov Processes",
    booktitle="Proc. 30th Conf. Mathematical Foundations of Programming Semantics (MFPS'14)",
    editor="Bart Jacobs and Alexandra Silva and Sam Staton",
    publisher="Elsevier",
    series="Electronic Notes in Theoretical Computer Science",
    month="June",
    year="2014",
    pages="215--231"
  }

  We extend our previous duality theorem for Markov processes by equipping the processes with a pseudometric and the algebras with a notion of metric diameter. We are able to show that the isomorphisms of our previous duality theorem become isometries in this quantitative setting. This opens the way to developing theories of approximate reasoning for probabilistic systems.

• Henk Barendregt, Venanzio Capretta, and Dexter Kozen. Reflection in the Chomsky hierarchy. J. Automata, Languages and Combinatorics, 18(1):53-60, 2013.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{BCK13a,
    author="Henk Barendregt and Venanzio Capretta and Dexter Kozen",
    title="Reflection in the {C}homsky Hierarchy",
    journal="J. Automata, Languages and Combinatorics",
    volume="18",
    number="1",
    pages="53--60",
    year="2013"
  }

  We investigate which classes of formal languages in the Chomsky hierarchy are reflexive, that is, contain a language of codes that is universal for the whole class.

• Dexter Kozen and Konstantinos Mamouras. Kleene algebra with products and iteration theories. In Simona Ronchi Della Rocca, editor, Proc. 22nd EACSL Conf. Computer Science Logic (CSL'13), volume 23 of Leibniz International Proceedings in Informatics (LIPIcs), pages 415-431, Torino, Italy, September 2013. Dagstuhl Publishing.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KM13a,
    author="Dexter Kozen and Konstantinos Mamouras",
    title="{K}leene Algebra with Products and Iteration Theories",
    booktitle="Proc. 22nd EACSL Conf. Computer Science Logic (CSL'13)",
    editor="Simona Ronchi Della Rocca",
    month="September",
    year="2013",
    pages="415--431",
    address="Torino, Italy",
    series="Leibniz International Proceedings in Informatics (LIPIcs)",
    publisher="Dagstuhl Publishing",
    volume="23"
  }

  We develop a typed equational system that subsumes both iteration theories and typed Kleene algebra in a common framework. Our approach is based on cartesian categories endowed with commutative strong monads to handle nondeterminism.

• Niels Bjørn Bugge Grathwohl, Fritz Henglein, and Dexter Kozen. Infinitary axiomatization of the equational theory of context-free languages. In David Baelde and Arnaud Carayol, editors, Proc. 9th Workshop Fixed Points in Computer Science (FICS 2013), volume 126 of Electronic Proceedings in Theoretical Computer Science, pages 44-55, Torino, Italy, September 2013. (Subsumed by Niels Bjørn Bugge Grathwohl, Fritz Henglein, and Dexter Kozen. Infinitary axiomatization of the equational theory of context-free languages. Fundamenta Informaticae, 150:241-257, 2017. doi:10.3233/FI-2017-1469.)
  [abstract] [bibtex] []

  @inproceedings{GHK13a,
    author="Niels Bj{\o}rn Bugge Grathwohl and Fritz Henglein and Dexter Kozen",
    title="Infinitary Axiomatization of the Equational Theory of Context-Free Languages",
    booktitle="Proc.~9th Workshop Fixed Points in Computer Science (FICS 2013)",
    editor="David Baelde and Arnaud Carayol",
    month="September",
    year="2013",
    pages="44--55",
    address="Torino, Italy",
    series="Electronic Proceedings in Theoretical Computer Science",
    volume="126"
  }

  We give a natural complete infinitary axiomatization of the equational theory of the context-free languages, answering a question of Leiss (1992).

• Dexter Kozen, Radu Mardare, and Prakash Panangaden. Strong completeness for Markovian logics. In Krishnendu Chatterjee and Jirí Sgall, editors, Proc. 38th Symp. Mathematical Foundations of Computer Science (MFCS 2013), volume 8087 of Lect. Notes in Computer Science, pages 655-666, Klosterneuburg, Austria, August 2013. Springer.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KMP13a,
    author="Dexter Kozen and Radu Mardare and Prakash Panangaden",
    title="Strong Completeness for {M}arkovian Logics",
    booktitle="Proc. 38th Symp. Mathematical Foundations of Computer Science (MFCS 2013)",
    editor="Krishnendu Chatterjee and Jir\'i Sgall",
    pages="655--666",
    month="August",
    year="2013",
    address="Klosterneuburg, Austria",
    publisher="Springer",
    series="Lect. Notes in Computer Science",
    volume="8087"
  }

  In this paper we present Hilbert-style axiomatizations for three logics for reasoning about continuous-space Markov processes (MPs): (i) a logic for MPs defined for probability distributions on measurable state spaces, (ii) a logic for MPs defined for sub-probability distributions and (iii) a logic defined for arbitrary distributions. These logics are not compact so one needs infinitary rules in order to obtain strong completeness results.
  We propose a new infinitary rule that replaces the so-called Countable Additivity Rule (CAR) currently used in the literature to address the problem of proving strong completeness for these and similar logics. Unlike the CAR, our rule has a countable set of instances; consequently it allows us to apply the Rasiowa-Sikorski lemma for establishing strong completeness. Our proof method is novel and it can be used for other logics as well.

• Dexter Kozen, Kim G. Larsen, Radu Mardare, and Prakash Panangaden. Stone duality for Markov processes. In Orna Kupferman, editor, Proc. 28th IEEE/ACM Symp. Logic in Computer Science (LICS 2013), pages 321-330, New Orleans, June 2013. IEEE/ACM.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KLMP13a,
    author="Dexter Kozen and Kim G.~Larsen and Radu Mardare and Prakash Panangaden",
    title="Stone Duality for {M}arkov Processes",
    booktitle="Proc. 28th IEEE/ACM Symp. Logic in Computer Science (LICS 2013)",
    editor="Orna Kupferman",
    pages="321--330",
    month="June",
    year="2013",
    address="New Orleans",
    publisher="IEEE/ACM"
  }

  We define Aumann algebras, an algebraic analog of probabilistic modal logic. An Aumann algebra consists of a Boolean algebra with operators modeling probabilistic transitions. We prove that countable Aumann algebras and countably-generated continuous-space Markov processes are dual in the sense of Stone. Our results subsume existing results on completeness of probabilistic modal logics for Markov processes.

• Dexter Kozen and Alexandra Silva. Practical coinduction. Technical Report http://hdl.handle.net/1813/30510, Computing and Information Science, Cornell University, November 2012. (Subsumed by Dexter Kozen and Alexandra Silva. Practical coinduction. Mathematical Structures in Computer Science, 27:1132-1152, 2017. doi:10.1017/S0960129515000493.)
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{KS12b,
    author="Dexter Kozen and Alexandra Silva",
    title="Practical Coinduction",
    institution="Computing and Information Science, Cornell University",
    number="{\url{http://hdl.handle.net/1813/30510}}",
    month="November",
    year="2012"
  }

  Induction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively-defined datatypes such as finite lists, finite trees, and the natural numbers. Coinduction is the dual principle that can be used to reason about coinductive datatypes such as infinite streams or trees, but it is not as widespread or as well understood. In this paper, we illustrate through several examples the use of coinduction in informal mathematical arguments. Our aim is to promote the principle as a useful tool for the working mathematician and to bring it to a level of familiarity on par with induction. We show that coinduction is not only about bisimilarity and equality of behaviors, but also applicable to a variety of functions and relations defined on coinductive datatypes.

• Dexter Kozen and Alexandra Silva. Left-handed completeness. In Wolfram Kahl and Timothy G. Griffin, editors, Proc. Conf. Relational and Algebraic Methods in Computer Science (RAMiCS 2012), volume 7560 of Lecture Notes in Computer Science, pages 162-178, Cambridge, UK, September 2012. Springer. (Subsumed by Dexter Kozen and Alexandra Silva. Left-handed completeness. Theoretical Computer Science, 807:220-233, 6 February 2020. URL: http://www.sciencedirect.com/science/article/pii/S0304397519306838, doi:10.1016/j.tcs.2019.10.040.)
  [abstract] [bibtex] []

  @inproceedings{KS12a,
    author="Dexter Kozen and Alexandra Silva",
    title="Left-Handed Completeness",
    booktitle="Proc. Conf. Relational and Algebraic Methods in Computer Science (RAMiCS 2012)",
    editor="Wolfram Kahl and Timothy G. Griffin",
    month="September",
    year="2012",
    address="Cambridge, UK",
    publisher="Springer",
    series="Lecture Notes in Computer Science",
    volume="7560",
    pages="162--178"
  }

  We give a new, significantly shorter proof of the completeness of the left-handed star rule of Kleene algebra. The proof exposes the rich interaction of algebra and coalgebra in the theory of Kleene algebra.

• Jean-Baptiste Jeannin and Dexter Kozen. Capsules and separation. In Nachum Dershowitz, editor, Proc. 27th ACM/IEEE Symp. Logic in Computer Science (LICS'12), pages 425-430, Dubrovnik, Croatia, June 2012. IEEE.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{JK12a,
    author="Jean-Baptiste Jeannin and Dexter Kozen",
    title="Capsules and Separation",
    booktitle="Proc. 27th ACM/IEEE Symp. Logic in Computer Science (LICS'12)",
    editor="Nachum Dershowitz",
    month="June",
    year="2012",
    address="Dubrovnik, Croatia",
    pages="425--430",
    publisher="IEEE"
  }

  We study a formulation of separation logic using capsules, a representation of the state of a computation in higher-order programming languages with mutable variables. We prove soundness of the frame rule in this context and investigate alternative formulations with weaker side conditions.

• Dexter Kozen. New. In Ulrich Berger and Michael Mislove, editors, Proc. 28th Conf. Math. Found. Programming Semantics (MFPS XXVIII), pages 13-38, Bath, England, June 2012. Elsevier Electronic Notes in Theoretical Computer Science.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{K12a,
    author="Dexter Kozen",
    title="New",
    booktitle="Proc. 28th Conf. Math. Found. Programming Semantics (MFPS XXVIII)",
    editor="Ulrich Berger and Michael Mislove",
    month="June",
    year="2012",
    address="Bath, England",
    pages="13--38",
    publisher="Elsevier Electronic Notes in Theoretical Computer Science"
  }

  We propose a theoretical device for modeling the creation of new indiscernible semantic objects during program execution. The method fits well with the semantics of imperative, functional, and object-oriented languages and promotes equational reasoning about higher-order state.

• Dexter Kozen and Ganesh Ramanarayanan. Publication/citation: A proof-theoretic approach to mathematical knowledge management. In Johan van Benthem, Amitabha Gupta, and Eric Pacuit, editors, Games, Norms, and Reasons: Logic at the Crossroads, volume 353 of Synthese Library, pages 151-161. Dordrecht, Springer Science and Business Media, 2011.
  [full text (.pdf)] [abstract] [bibtex] []

  @incollection{KR11a,
    author="Dexter Kozen and Ganesh Ramanarayanan",
    title="Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge Management",
    booktitle="Games, Norms, and Reasons: Logic at the Crossroads",
    editor="Johan van Benthem and Amitabha Gupta and Eric Pacuit",
    publisher="Dordrecht, Springer Science and Business Media",
    series="Synthese Library",
    volume="353",
    pages="151--161",
    year="2011"
  }

  There are many real-life examples of formal systems that support constructions or proofs, but that do not provide direct support for remembering them so that they can be recalled and reused in the future. In this paper we examine the operations of publication (remembering a proof) and citation (recalling a proof for reuse), regarding them as forms of common subexpression elimination on proof terms. We then develop this idea from a proof theoretic perspective, describing a simple complete proof system for universal Horn equational logic using three new proof rules, publish, cite and forget. These rules can provide a proof-theoretic infrastructure for proof reuse in any system.

• Dexter Kozen. Halting and equivalence of program schemes in models of arbitrary theories. In Andreas Blass, Nachum Dershowitz, and Wolfgang Reisig, editors, Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, volume 6300 of Lecture Notes in Computer Science, pages 463-469. Springer-Verlag, August 2010.
  [full text (.pdf)] [abstract] [bibtex] []

  @incollection{K10b,
    author="Dexter Kozen",
    title="Halting and Equivalence of Program Schemes in Models of Arbitrary Theories",
    booktitle="Fields of Logic and Computation: Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday",
    editor="Andreas Blass and Nachum Dershowitz and Wolfgang Reisig",
    series="Lecture Notes in Computer Science",
    volume="6300",
    publisher="Springer--Verlag",
    month="August",
    year="2010",
    pages="463--469"
  }

  In this note we consider the following decision problems. Let $\Sigma$ be a fixed first-order signature.
  
  (i) Given a first-order theory or ground theory $T$ over $\Sigma$ of Turing degree $\alpha$, a program scheme $p$ over $\Sigma$, and input values specified by ground terms $t_1,\ldots,t_n$, does $p$ halt on input $t_1,\ldots,t_n$ in all models of $T$?
  
  (ii) Given a first-order theory or ground theory $T$ over $\Sigma$ of Turing degree $\alpha$ and two program schemes $p$ and $q$ over $\Sigma$, are $p$ and $q$ equivalent in all models of $T$?
  
  When $T$ is empty, these two problems are the classical halting and equivalence problems for program schemes, respectively. We show that problem (i) is $\Sigma^\alpha_1$-complete and problem (ii) is $\Pi^\alpha_2$-complete. Both problems remain hard for their respective complexity classes even if $\Sigma$ is restricted to contain only a single constant, a single unary function symbol, and a single monadic predicate. It follows from (ii) that there can exist no relatively complete deductive system for scheme equivalence over models of theories of any Turing degree.

• Dexter Kozen. Church-Rosser made easy. Fundamenta Informaticae, 103:129-136, 2010.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K10a,
    author="Dexter Kozen",
    title="Church-{R}osser Made Easy",
    journal="Fundamenta Informaticae",
    volume="103",
    pages="129--136",
    year="2010"
  }

  The Church–Rosser theorem states that the λ-calculus is confluent under β-reductions. The standard proof of this result is due to Tait and Martin-Löf. In this note, we present an alternative proof based on the notion of acceptable orderings. The technique is easily modified to give confluence of the βη-calculus.

• Dexter Kozen. Nonlocal flow of control and Kleene algebra with tests. In Proc. 23rd IEEE Symp. Logic in Computer Science (LICS'08), pages 105-117, June 2008.
  [full text] [abstract] [bibtex] []

  @inproceedings{K08b,
    author="Dexter Kozen",
    title="Nonlocal Flow of Control and {K}leene Algebra with Tests",
    booktitle="Proc. 23rd IEEE Symp. Logic in Computer Science (LICS'08)",
    month="June",
    year="2008",
    city="Pittsburgh",
    pages="105--117"
  }

  Kleene algebra with tests (KAT) is an equational system for program verification that combines Kleene algebra (KA), or the algebra of regular expressions, with Boolean algebra. It can model basic programming and verification constructs such as conditional tests, while loops, and Hoare triples, thus providing a relatively simple equational approach to program equivalence and partial correctness. In this paper we show how KAT can be used to give a rigorous equational treatment of control constructs involving nonlocal transfer of control such as unconditional jumps, loop statements with multi-level breaks, and exception handlers. We develop a compositional semantics and a complete equational axiomatization. The approach has some novel technical features, including a treatment of multi-level break statements that is reminiscent of de Bruijn indices in the variable-free lambda calculus. We illustrate the use of the system by giving a purely calculational proof that every deterministic flowchart is equivalent to a loop program with multi-level breaks.

• Dexter Kozen and Wei-Lung (Dustin) Tseng. The Böhm-Jacopini theorem is false, propositionally. In P. Audebaud and C. Paulin-Mohring, editors, Proc. 9th Int. Conf. Mathematics of Program Construction (MPC'08), volume 5133 of Lecture Notes in Computer Science, pages 177-192. Springer, July 2008.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KT08a,
    author="Dexter Kozen and Wei-Lung (Dustin) Tseng",
    title="The {B\"o}hm-{J}acopini Theorem is False, Propositionally",
    booktitle="Proc. 9th Int. Conf. Mathematics of Program Construction (MPC'08)",
    editor="P. Audebaud and C. Paulin-Mohring",
    month="July",
    year="2008",
    publisher="Springer",
    series="Lecture Notes in Computer Science",
    volume="5133",
    pages="177--192"
  }

  The Böhm-Jacopini theorem (Böhm and Jacopini, 1966) is a classical result of program schematology. It states that any deterministic flowchart program is equivalent to a while program. The theorem is usually formulated at the first-order interpreted or first-order uninterpreted (schematic) level, because the construction requires the introduction of auxiliary variables. Ashcroft and Manna (1972) and Kosaraju (1973) showed that this is unavoidable. As observed by a number of authors, a slightly more powerful structured programming construct, namely loop programs with multi-level breaks, is sufficient to represent all deterministic flowcharts without introducing auxiliary variables. Kosaraju (1973) established a strict hierarchy determined by the maximum level of the multi-level breaks that are allowed. In this paper we give purely propositional account of these results. We reformulate the problems at the propositional level in terms of automata on guarded strings, the automata-theoretic counterpart to Kleene algebra with tests. Whereas the classical approaches do not distinguish the first-order and propositional level of abstraction, we find that the purely propositional formulation allows a more streamlined mathematical treatment, using algebraic and topological concepts such as bisimulation and coinduction. Using these tools, we can give more mathematically rigorous formulations and simpler and more revealing proofs.

• Kamal Aboul-Hosn and Dexter Kozen. Local variable scoping and Kleene algebra with tests. J. Log. Algebr. Program., 2007. doi:10.1016/j.jlap.2007.10.007.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{AK07a,
    author="Kamal Aboul-Hosn and Dexter Kozen",
    title="Local Variable Scoping and {K}leene Algebra with Tests",
    journal="J. Log. Algebr. Program. ",
    year="2007",
    doi="10.1016/j.jlap.2007.10.007"
  }

  Most previous work on the semantics of programs with local state involves complex storage modeling with pointers and memory cells, complicated categorical constructions, or reasoning in the presence of context. In this paper, we explore the extent to which relational semantics and axiomatic reasoning in the style of Kleene algebra can be used to avoid these complications. We provide (i) a fully compositional relational semantics for a first-order programming language with a construct for local variable scoping; and (ii) an equational proof system based on Kleene algebra with tests for proving equivalence of programs in this language. We show that the proof system is sound and complete relative to the underlying equational theory without local scoping. We illustrate the use of the system with several examples.

• Dexter Kozen. Coinductive proof principles for stochastic processes. Logical Methods in Computer Science, 3(4:8), 2007. doi:10.2168/LMCS-3(4:8)2007.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K07b,
    author="Dexter Kozen",
    title="Coinductive Proof Principles for Stochastic Processes",
    journal="Logical Methods in Computer Science",
    volume="3",
    number="4:8",
    year="2007",
    doi="10.2168/LMCS-3(4:8)2007"
  }

  We give an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique. The rule encapsulates low-level analytic arguments, allowing reasoning about such processes at a higher algebraic level. We illustrate the use of the rule in deriving properties of a simple coin-flip process.

• Dexter Kozen and Marc Timme. Indefinite summation and the Kronecker delta. Technical Report http://hdl.handle.net/1813/8352, Computing and Information Science, Cornell University, October 2007.
  [full text] [abstract] [bibtex] []

  @techreport{KT07b,
    author="Dexter Kozen and Marc Timme",
    title="Indefinite Summation and the {K}ronecker Delta",
    institution="Computing and Information Science, Cornell University",
    number="{\url{http://hdl.handle.net/1813/8352}}",
    month="October",
    year="2007"
  }

  Indefinite summation, together with a generalized version of the Kronecker delta, provide a calculus for reasoning about various polynomial functions that arise in combinatorics, such as the Tutte, chromatic, flow, and reliability polynomials. In this paper we develop the algebraic properties of the indefinite summation operator and the generalized Kronecker delta from an axiomatic viewpoint. Our main result is that the axioms are equationally complete; that is, all equations that hold under the intended interpretations are derivable in the calculus.

• Dexter Kozen and Nicholas Ruozzi. Applications of metric coinduction. Logical Methods in Computer Science, 5(3), September 2009. doi:10.2168/LMCS-5(3:10)2009.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KR09,
    author="Dexter Kozen and Nicholas Ruozzi",
    title="Applications of Metric Coinduction",
    journal="Logical Methods in Computer Science",
    month="September",
    year="2009",
    volume="5",
    number="3",
    doi="10.2168/LMCS-5(3:10)2009"
  }

  Metric coinduction is a form of coinduction that can be used to establish properties of objects constructed as a limit of finite approximations. One can prove a coinduction step showing that some property is preserved by one step of the approximation process, then automatically infer by the coinduction principle that the property holds of the limit object. This can often be used to avoid complicated analytic arguments involving limits and convergence, replacing them with simpler algebraic arguments. This paper examines the application of this principle in a variety of areas, including infinite streams, Markov chains, Markov decision processes, and non-well-founded sets. These results point to the usefulness of coinduction as a general proof technique.

• Dexter Kozen and Nicholas Ruozzi. Applications of metric coinduction. In T. Mossakowski et al., editor, Proc. 2nd Conf. Algebra and Coalgebra in Computer Science (CALCO 2007), volume 4624 of Lecture Notes in Computer Science, pages 327-341. Springer, August 2007. (Subsumed by Dexter Kozen and Nicholas Ruozzi. Applications of metric coinduction. Logical Methods in Computer Science, 5(3), September 2009. doi:10.2168/LMCS-5(3:10)2009.)
  [bibtex] []

  @inproceedings{KR07a,
    author="Dexter Kozen and Nicholas Ruozzi",
    title="Applications of Metric Coinduction",
    booktitle="Proc. 2nd Conf. Algebra and Coalgebra in Computer Science (CALCO 2007)",
    editor="T. Mossakowski et al.",
    month="August",
    year="2007",
    series="Lecture Notes in Computer Science",
    volume="4624",
    publisher="Springer",
    city="Bergen, Norway",
    pages="327--341"
  }

• Kamal Aboul-Hosn and Dexter Kozen. Local variable scoping and Kleene algebra with tests. In R. A. Schmidt, editor, Proc. 9th Int. Conf. Relational Methods in Computer Science and 4th Int. Workshop Applications of Kleene Algebra (RelMiCS/AKA'06), volume 4136 of Lecture Notes in Computer Science, pages 78-90. Springer, August 2006. (Subsumed by Kamal Aboul-Hosn and Dexter Kozen. Local variable scoping and Kleene algebra with tests. J. Log. Algebr. Program., 2007. doi:10.1016/j.jlap.2007.10.007.)
  [bibtex] []

  @inproceedings{AK06c,
    author="Kamal Aboul-Hosn and Dexter Kozen",
    title="Local Variable Scoping and {K}leene Algebra with Tests",
    booktitle="Proc. 9th Int. Conf. Relational Methods in Computer Science and 4th Int. Workshop Applications of Kleene Algebra (RelMiCS/AKA'06)",
    editor="R. A. Schmidt",
    month="August",
    year="2006",
    series="Lecture Notes in Computer Science",
    volume="4136",
    publisher="Springer",
    city="Manchester, UK",
    pages="78--90"
  }

• Dexter Kozen. On the representation of Kleene algebras with tests. In R. Královic and P. Urzyczyn, editors, Proc. Conf. Mathematical Foundations of Computer Science (MFCS'06), volume 4162 of Lecture Notes in Computer Science, pages 73-83. Springer, August 2006.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{K06c,
    author="Dexter Kozen",
    title="On the Representation of {K}leene Algebras with Tests",
    booktitle="Proc. Conf. Mathematical Foundations of Computer Science (MFCS'06)",
    editor="R. Kr\'{a}lovic and P. Urzyczyn",
    series="Lecture Notes in Computer Science",
    publisher="Springer",
    volume="4162",
    month="August",
    year="2006",
    pages="73--83"
  }

  We investigate conditions under which a given Kleene algebra with tests is isomorphic to an algebra of binary relations. Two simple separation properties are identified that, along with star-continuity, are sufficient for nonstandard relational representation. An algebraic condition is identified that is necessary and sufficient for the construction to produce a standard representation.

• Dexter Kozen. Coinductive proof principles for stochastic processes. In Rajeev Alur, editor, Proc. 21st Symp. Logic in Computer Science (LICS'06), pages 359-366. IEEE, August 2006. (Subsumed by Dexter Kozen. Coinductive proof principles for stochastic processes. Logical Methods in Computer Science, 3(4:8), 2007. doi:10.2168/LMCS-3(4:8)2007.)
  [bibtex] []

  @inproceedings{K06b,
    author="Dexter Kozen",
    title="Coinductive Proof Principles for Stochastic Processes",
    booktitle="Proc. 21st Symp. Logic in Computer Science (LICS'06)",
    organization="IEEE",
    city="Seattle, WA",
    editor="Rajeev Alur",
    month="August",
    year="2006",
    pages="359--366"
  }

• Kamal Aboul-Hosn and Dexter Kozen. Relational semantics for higher-order programs. In Tarmo Uustalu, editor, Proc. 8th Int. Conf. Mathematics of Program Construction (MPC'06), volume 4014 of Lecture Notes in Computer Science, pages 29-48. Springer, July 2006.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{AK06b,
    author="Kamal Aboul-Hosn and Dexter Kozen",
    title="Relational Semantics for Higher-Order Programs",
    booktitle="Proc. 8th Int. Conf. Mathematics of Program Construction (MPC'06)",
    editor="Tarmo Uustalu",
    series="Lecture Notes in Computer Science",
    volume="4014",
    publisher="Springer",
    month="July",
    year="2006",
    city="Kuressaare, Estonia",
    pages="29--48"
  }

  Most previous work on the semantics of higher-order programs with local state involves complex storage modeling with pointers and memory cells, complicated categorical constructions, or reasoning in the presence of context. In this paper we show how a relatively simple relational semantics can be used to avoid these complications. We provide a natural relational semantics for a programming language with higher-order functions. The semantics is purely compositional, with all contextual considerations completely encapsulated in the state. We show several equivalence proofs using this semantics based on examples of Meyer and Sieber (1988).

• Dexter Kozen, Christoph Kreitz, and Eva Richter. Automating proofs in category theory. In Proc. 3rd Int. Joint Conf. Automated Reasoning (IJCAR'06), number 4130 in Lecture Notes in AI, pages 392-407. Springer, August 2006.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KKR06a,
    author="Dexter Kozen and Christoph Kreitz and Eva Richter",
    title="Automating Proofs in Category Theory",
    booktitle="Proc. 3rd Int. Joint Conf. Automated Reasoning (IJCAR'06)",
    series="Lecture Notes in AI",
    number="4130",
    publisher="Springer",
    city="Seattle, WA",
    month="August",
    year="2006",
    pages="392--407"
  }

  We introduce a semi-automated proof system for basic category-theoretic reasoning. It is based on a first-order sequent calculus that captures the basic properties of categories, functors and natural transformations as well as a small set of proof tactics that automate proof search in this calculus. We demonstrate our approach by automating the proof that the functor categories Fun[CxD,E] and Fun[C,Fun[D,E]] are naturally isomorphic.

• Kamal Aboul-Hosn and Dexter Kozen. KAT-ML: An interactive theorem prover for Kleene algebra with tests. Journal of Applied Non-Classical Logics, 16(1-2):9-33, 2006.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{AK06a,
    author="Kamal Aboul-Hosn and Dexter Kozen",
    title="{KAT-ML}: An Interactive Theorem Prover for {K}leene Algebra with Tests",
    journal="Journal of Applied Non-Classical Logics",
    volume="16",
    number="1--2",
    year="2006",
    pages="9--33"
  }

  We describe KAT-ML, an implementation of an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. One can also use the system to reason about properties of simple imperative programs using schematic KAT (SKAT). We explain how the system works and illustrate its use with some examples, including an extensive scheme equivalence proof.

• Dexter Kozen and Bernhard Möller. Separability in domain semirings. Technical Report 2004-16, Universität Augsburg, Institut für Informatik, December 2004.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{KM04,
    author="Dexter Kozen and Bernhard M{\"o}ller",
    title="Separability in Domain Semirings",
    institution="Universit{\"a}t Augsburg, Institut f{\"u}r Informatik",
    month="December",
    year="2004",
    number="2004-16"
  }

  First, we show with two examples that in test semirings with an incomplete test algebra a domain operation may or may not exist. Second, we show that two notions of separability in test semirings coincide, respectively, with locality of composition and with extensionality of the diamond operators in domain semirings. We conclude with a brief comparison of dynamic algebras and modal Kleene algebras.

• Dexter Kozen. Toward the automation of category theory. Technical Report TR2004-1964, Computer Science Department, Cornell University, September 2004.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{K04e,
    author="Dexter Kozen",
    title="Toward the Automation of Category Theory",
    institution="Computer Science Department, Cornell University",
    number="TR2004-1964",
    month="September",
    year="2004"
  }

  We introduce a sequent system for basic category-theoretic reasoning suitable for computer implementation. We illustrate its use by giving a complete formal proof that the functor categories Fun[CxD,E] and Fun[C,Fun[D,E]] are naturally isomorphic.

• Dexter Kozen. Natural transformations as rewrite rules and monad composition. Technical Report TR2004-1942, Computer Science Department, Cornell University, July 2004. (Subsumed by Dexter Kozen. Natural transformations as rewrite rules and monad composition. Logical Methods in Computer Science, 15(1):1-12, January 2019. doi:10.23638/LMCS-15(1:1)2019.)
  [abstract] [bibtex] []

  @techreport{K04c,
    author="Dexter Kozen",
    title="Natural Transformations as Rewrite Rules and Monad Composition",
    institution="Computer Science Department, Cornell University",
    number="TR2004-1942",
    month="July",
    year="2004"
  }

  Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a different approach involving string rewriting. We show that a given tuple (T,mu,eta) is a monad if and only if T is a terminal object in a certain category of functors and natural transformations, and that this fact can be established by proving confluence of a certain string rewriting system. We illustrate the technique on the monad composition problem of Eklund et al.

• Dexter Kozen. Some results in dynamic model theory. Science of Computer Programming, 51(1-2):3-22, May 2004. Special issue: Mathematics of Program Construction (MPC 2002). Eerke Boiten and Bernhard Möller (eds.). doi:10.1016/j.scico.2003.09.004.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K04b,
    author="Dexter Kozen",
    title="Some Results in Dynamic Model Theory",
    journal="Science of Computer Programming",
    volume="51",
    number="1--2",
    month="May",
    year="2004",
    pages="3--22",
    doi="10.1016/j.scico.2003.09.004",
    note="Special issue: {\em Mathematics of Program Construction (MPC 2002)}. Eerke Boiten and Bernhard M{\"o}ller (eds.)"
  }

  First-order structures over a fixed signature $\Sigma$ give rise to a family of trace-based and relational Kleene algebras with tests defined in terms of Tarskian frames. A Tarskian frame is a Kripke frame whose states are valuations of program variables and whose atomic actions are state changes effected by variable assignments $x := e$, where $e$ is a $\Sigma$-term. The Kleene algebras with tests that arise in this way play a role in dynamic model theory akin to the role played by Lindenbaum algebras in classical first-order model theory. Given a first-order theory $T$ over $\Sigma$, we exhibit a Kripke frame $U$ whose trace algebra $\mathrm{Tr}_U$ is universal for the equational theory of Tarskian trace algebras over $\Sigma$ satisfying $T$, although $U$ itself is not Tarskian in general. The corresponding relation algebra Rel$_U$ is not universal for the equational theory of relation algebras of Tarskian frames, but it is so modulo observational equivalence.

• Dexter Kozen. Computational inductive definability. Annals of Pure and Applied Logic, 126(1-3):139-148, April 2004. Special issue: Provinces of logic determined. Essays in the memory of Alfred Tarski. Zofia Adamowicz, Sergei Artemov, Damian Niwinski, Ewa Orlowska, Anna Romanowska, and Jan Wolenski (eds.). doi:10.1016/j.apal.2003.10.013.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K04a,
    author="Dexter Kozen",
    title="Computational Inductive Definability",
    journal="Annals of Pure and Applied Logic",
    volume="126",
    number="1--3",
    month="April",
    year="2004",
    pages="139--148",
    doi="10.1016/j.apal.2003.10.013",
    note="Special issue: {\em Provinces of logic determined. Essays in the memory of Alfred Tarski}. Zofia Adamowicz, Sergei Artemov, Damian Niwinski, Ewa Orlowska, Anna Romanowska, and Jan Wolenski (eds.)"
  }

  It is shown that over any countable first-order structure, IND programs with dictionaries accept exactly the $\Pi_1^1$ relations. This extends a result of Harel and Kozen (1984) relating IND and $\Pi_1^1$ over countable structures with some coding power, and provides a computational analog of a result of Barwise, Gandy, and Moschovakis (1971) relating the $\Pi_1^1$ relations on a countable structure to a certain family of inductively definable relations on the hereditarily finite sets over that structure.

• Kamal Aboul-Hosn and Dexter Kozen. KAT-ML: An interactive theorem prover for Kleene algebra with tests. In Boris Konev and Renate Schmidt, editors, Proc. 4th Int. Workshop on the Implementation of Logics (WIL'03), pages 2-12. University of Manchester, September 2003. (Subsumed by Kamal Aboul-Hosn and Dexter Kozen. KAT-ML: An interactive theorem prover for Kleene algebra with tests. Journal of Applied Non-Classical Logics, 16(1-2):9-33, 2006.)
  [bibtex] []

  @inproceedings{AK03a,
    author="Kamal Aboul-Hosn and Dexter Kozen",
    title="{KAT-ML}: An Interactive Theorem Prover for {K}leene Algebra with Tests",
    booktitle="Proc. 4th Int. Workshop on the Implementation of Logics (WIL'03)",
    editor="Boris Konev and Renate Schmidt",
    city="Almaty, Kazakhstan",
    month="September",
    year="2003",
    publisher="University of Manchester",
    pages="2--12"
  }

• Chris Hardin and Dexter Kozen. On the complexity of the Horn theory of REL. Technical Report TR2003-1896, Computer Science Department, Cornell University, May 2003.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{HK03a,
    author="Chris Hardin and Dexter Kozen",
    title="On the complexity of the {H}orn theory of {REL}",
    institution="Computer Science Department, Cornell University",
    number="TR2003-1896",
    month="May",
    year="2003"
  }

  We show that the universal Horn theory of relational Kleene algebras is $\Pi_1^1$-complete.

• Dexter Kozen and Jerzy Tiuryn. Substructural logic and partial correctness. Trans. Computational Logic, 4(3):355-378, July 2003.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KT03a,
    author="Dexter Kozen and Jerzy Tiuryn",
    title="Substructural Logic and Partial Correctness",
    journal="Trans. Computational Logic",
    volume="4",
    number="3",
    month="July",
    year="2003",
    pages="355--378"
  }

  We formulate a noncommutative sequent calculus for partial correctness that subsumes propositional Hoare Logic. Partial correctness assertions are represented by intuitionistic linear implication. We prove soundness and completeness over relational and trace models. As a corollary we obtain a complete sequent calculus for inclusion and equivalence of regular expressions.

• Dexter Kozen. On Hoare logic, Kleene algebra, and types. In P. Gärdenfors, J. Wole\'nski, and K. Kijania-Placek, editors, In the Scope of Logic, Methodology, and Philosophy of Science: Volume 1 of the 11th Int. Congress Logic, Methodology and Philosophy of Science, Cracow, August 1999, volume 315 of Studies in Epistemology, Logic, Methodology, and Philosophy of Science, pages 119-133. Kluwer, 2002.
  [full text (.pdf)] [abstract] [bibtex] []

  @incollection{K02g,
    author="Dexter Kozen",
    title="On {H}oare logic, {K}leene algebra, and types",
    booktitle="In the Scope of Logic, Methodology, and Philosophy of Science: Volume 1 of the 11th Int. Congress Logic, Methodology and Philosophy of Science, Cracow, August 1999",
    publisher="Kluwer",
    series="Studies in Epistemology, Logic, Methodology, and Philosophy of Science",
    volume="315",
    editor="P. G{\"a}rdenfors and J. Wole{\'n}ski and K. Kijania-Placek",
    pages="119--133",
    year="2002"
  }

  We show that propositional Hoare logic is subsumed by the type calculus of typed Kleene algebra augmented with subtypes and typecasting. Assertions are interpreted as typecast operators. Thus Hoare-style reasoning with partial correctness assertions reduces to typechecking in this system.

• Dexter Kozen. On the complexity of reasoning in Kleene algebra. Information and Computation, 179:152-162, 2002.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K02f,
    title="On the complexity of reasoning in {K}leene algebra",
    author="Dexter Kozen",
    journal="Information and Computation",
    volume="179",
    year="2002",
    pages="152--162"
  }

  We study the complexity of reasoning in Kleene algebra and *-continuous Kleene algebra in the presence of extra assumptions; i.e., the complexity of deciding the validity of universal Horn formulas $E \to s=t$, where $E$ is a finite set of equations. We obtain various levels of complexity based on the form of the assumptions $E$. Our main results are: for *-continuous Kleene algebra,
  
  1. if $E$ contains only commutativity assumptions $pq=qp$, the problem is $\Pi^0_1$-complete (co-r.e. complete);
  2. if $E$ contains only monoid equations, the problem is $\Pi^0_2$-complete;
  3. for arbitrary equations $E$, the problem is $\Pi^1_1$-complete.
  
  The last problem is the universal Horn theory of the *-continuous Kleene algebras. This resolves an open question of [Kozen, LICS 1991].

• Dexter Kozen. Halting and equivalence of schemes over recursive theories. Technical Report TR2002-1881, Computer Science Department, Cornell University, October 2002.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{K02d,
    author="Dexter Kozen",
    title="Halting and Equivalence of Schemes over Recursive Theories",
    institution="Computer Science Department, Cornell University",
    number="TR2002-1881",
    month="October",
    year="2002"
  }

  Let $\Sigma$ be a fixed first-order signature. In this note we consider the following decision problems. (i) Given a recursive ground theory $T$ over $\Sigma$, a program scheme $p$ over $\Sigma$, and input values specified by ground terms $t_1,\ldots,t_n$, does $p$ halt on input $t_1,\ldots,t_n$ in all models of $T$? (ii) Given a recursive ground theory $T$ over $\Sigma$ and two program schemes $p$ and $q$ over $\Sigma$, are $p$ and $q$ equivalent in all models of $T$? When $T$ is empty, these two problems are the classical halting and equivalence problems for program schemes, respectively. We show that problem (i) is r.e.-complete and problem (ii) is $\Pi^0_2$-complete. Both these problems remain hard for their respective complexity classes even if $T$ is empty and $\Sigma$ is restricted to contain only a single constant, a single unary function symbol, and a single monadic predicate. It follows from (ii) that there can exist no relatively complete deductive system for scheme equivalence.

• Chris Hardin and Dexter Kozen. On the elimination of hypotheses in Kleene algebra with tests. Technical Report TR2002-1879, Computer Science Department, Cornell University, October 2002.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{HK02a,
    author="Chris Hardin and Dexter Kozen",
    title="On the Elimination of Hypotheses in {K}leene Algebra with Tests",
    institution="Computer Science Department, Cornell University",
    number="TR2002-1879",
    month="October",
    year="2002"
  }

  The validity problem for certain universal Horn formulas of Kleene algebra with tests (KAT) can be efficiently reduced to the equational theory. This reduction is known as elimination of hypotheses. Hypotheses are used to describe the interaction of atomic programs and tests and are an essential component of practical program verification with KAT. The ability to eliminate hypotheses of a certain form means that the Horn theory with premises of that form remains decidable in PSPACE. It was known (Cohen 1994, Kozen and Smith 1996, Kozen 1997) how to eliminate hypotheses of the form q=0. In this paper we show how to eliminate hypotheses of the form cp=c for atomic p. Hypotheses of this form are useful in eliminating redundant code and arise quite often in the verification of compiler optimizations (Kozen and Patron 2000).

• Adam Barth and Dexter Kozen. Equational verification of cache blocking in LU decomposition using Kleene algebra with tests. Technical Report TR2002-1865, Computer Science Department, Cornell University, June 2002.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{BK02a,
    author="Adam Barth and Dexter Kozen",
    title="Equational Verification of Cache Blocking in {LU} Decomposition using {K}leene Algebra with Tests",
    institution="Computer Science Department, Cornell University",
    number="TR2002-1865",
    month="June",
    year="2002"
  }

  In a recent paper of Mateev et al. (2001), a new technique for program analysis called fractal symbolic analysis was introduced and applied to verify the correctness of a series of source-level transformations for cache blocking in LU decomposition with partial pivoting. It was argued in that paper that traditional techniques are inadequate because the transformations break definition-use dependencies. We show how the task can be accomplished purely equationally using Kleene algebra with tests.

• Dexter Kozen. Some results in dynamic model theory. In E. A. Boiten and B. Möller, editors, Proc. Conf. Mathematics of Program Construction (MPC'02), volume 2386 of Lecture Notes in Computer Science, page 21. Springer-Verlag, July 2002. (Subsumed by Dexter Kozen. Some results in dynamic model theory. Science of Computer Programming, 51(1-2):3-22, May 2004. Special issue: Mathematics of Program Construction (MPC 2002). Eerke Boiten and Bernhard Möller (eds.). doi:10.1016/j.scico.2003.09.004.)
  [bibtex] []

  @inproceedings{K02c,
    author="Dexter Kozen",
    title="Some Results in Dynamic Model Theory",
    booktitle="Proc. Conf. Mathematics of Program Construction (MPC'02)",
    city="Dagstuhl, Germany",
    editor="E.~A.~Boiten and B.~M{\"o}ller",
    month="July",
    publisher="Springer-Verlag",
    series="Lecture Notes in Computer Science",
    volume="2386",
    pages="21",
    year="2002"
  }

• David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic logic. In D. M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume 4, pages 99-217. Kluwer, 2nd edition, 2002.
  [bibtex] []

  @incollection{HKT02a,
    title="Dynamic Logic",
    author="David Harel and Dexter Kozen and Jerzy Tiuryn",
    booktitle="Handbook of Philosophical Logic",
    volume="4",
    editor="D.~M.~Gabbay and F.~Guenthner",
    publisher="Kluwer",
    edition="2nd",
    year="2002",
    pages="99--217"
  }

• Allegra Angus and Dexter Kozen. Kleene algebra with tests and program schematology. Technical Report TR2001-1844, Computer Science Department, Cornell University, July 2001.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{AK01a,
    author="Allegra Angus and Dexter Kozen",
    title="Kleene Algebra with Tests and Program Schematology",
    institution="Computer Science Department, Cornell University",
    number="TR2001-1844",
    month="July",
    year="2001"
  }

  The theory of flowchart schemes has a rich history going back to Ianov (1960); see Manna (1974) for an elementary exposition. A central question in the theory of program schemes is scheme equivalence. Manna presents several examples of equivalence proofs that work by simplifying the schemes using various combinatorial transformation rules. In this paper we present a purely algebraic approach to this problem using Kleene algebra with tests (KAT). Instead of transforming schemes directly using combinatorial graph manipulation, we regard them as a certain kind of automaton on abstract traces. We prove a generalization of Kleene's theorem and use it to construct equivalent expressions in the language of KAT. We can then give a purely equational proof of the equivalence of the resulting expressions. We prove soundness of the method and give a detailed example of its use.

• Dexter Kozen and Jerzy Tiuryn. On the completeness of propositional Hoare logic. Information Sciences, 139(3-4):187-195, 2001.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KT01b,
    author="Dexter Kozen and Jerzy Tiuryn",
    title="On the completeness of propositional {H}oare logic",
    journal="Information Sciences",
    volume="139",
    number="3--4",
    year="2001",
    pages="187--195"
  }

  We investigate the completeness of Hoare Logic on the propositional level. In particular, the expressiveness requirements of Cook's proof are characterized propositionally. We give a completeness result for Propositional Hoare Logic (PHL): all relationally valid rules \[\frac{\{b_1\}p_1\{c_1\},\ldots,\{b_n\}p_n\{c_n\}}{\{b\}p\{c\}}\] are derivable in PHL, provided the propositional expressiveness conditions are met. Moreover, if the programs $p_i$ in the premises are atomic, no expressiveness assumptions are needed.

• Dexter Kozen and Jerzy Tiuryn. Intuitionistic linear logic and partial correctness. In Proc. 16th Symp. Logic in Comput. Sci. (LICS'01), pages 259-268. IEEE, June 2001. (Subsumed by Dexter Kozen and Jerzy Tiuryn. Substructural logic and partial correctness. Trans. Computational Logic, 4(3):355-378, July 2003.)
  [bibtex] []

  @inproceedings{KT01a,
    author="Dexter Kozen and Jerzy Tiuryn",
    title="Intuitionistic Linear Logic and Partial Correctness",
    booktitle="Proc. 16th Symp. Logic in Comput. Sci. (LICS'01)",
    organization="IEEE",
    city="Boston",
    month="June",
    year="2001",
    pages="259--268"
  }

• Roland Backhouse, Dexter Kozen, and Bernhard Möller, editors. Applications of Kleene Algebra, number 01081 in Dagstuhl Seminar Reports, February 2001.
  [bibtex] []

  @proceedings{BKM01,
    editor="Roland Backhouse and Dexter Kozen and Bernhard M{\"o}ller",
    title="Applications of Kleene Algebra",
    series="Dagstuhl Seminar Reports",
    number="01081",
    month="February",
    year="2001"
  }

• Dexter Kozen. Myhill-Nerode relations on automatic systems and the completeness of Kleene algebra. In Afonso Ferreira and Horst Reichel, editors, Proc. 18th Symp. Theoretical Aspects of Computer Science (STACS'01), volume 2010 of Lecture Notes in Computer Science, pages 27-38, Dresden, Germany, February 2001. Springer-Verlag.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{K01a,
    author="Dexter Kozen",
    title="Myhill-{N}erode Relations on Automatic Systems and the Completeness of {K}leene Algebra",
    booktitle="Proc. 18th Symp. Theoretical Aspects of Computer Science (STACS'01)",
    city="Dresden, Germany",
    address="Dresden, Germany",
    publisher="Springer-Verlag",
    series="Lecture Notes in Computer Science",
    volume="2010",
    editor="Afonso Ferreira and Horst Reichel",
    month="February",
    year="2001",
    pages="27--38"
  }

  It is well known that finite square matrices over a Kleene algebra again form a Kleene algebra. This is also true for infinite matrices under suitable restrictions. One can use this fact to solve certain infinite systems of inequalities over a Kleene algebra. Automatic systems are a special class of infinite systems that can be viewed as infinite-state automata. Automatic systems can be collapsed using Myhill-Nerode relations in much the same way that finite automata can. The Brzozowski derivative on an algebra of polynomials over a Kleene algebra gives rise to a triangular automatic system that can be solved using these methods. This provides an alternative method for proving the completeness of Kleene algebra.

• Ernie Cohen and Dexter Kozen. A note on the complexity of propositional Hoare logic. Trans. Computational Logic, 1(1):171-174, July 2000.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{CK00,
    author="Ernie Cohen and Dexter Kozen",
    title="A Note on the complexity of propositional {H}oare logic",
    journal="Trans. Computational Logic",
    volume="1",
    number="1",
    month="July",
    year="2000",
    pages="171--174"
  }

  We provide a simpler alternative proof of the PSPACE-hardness of propositional Hoare logic.

• David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. MIT Press, Cambridge, MA, 2000.
  [table of contents (.pdf)] [abstract] [bibtex] []

  @book{HKT00,
    author="David Harel and Dexter Kozen and Jerzy Tiuryn",
    title="Dynamic Logic",
    publisher="MIT Press",
    address="Cambridge, MA",
    year="2000",
    isbn="0-262-08289-6"
  }

  A graduate-level textbook on Dynamic Logic.

• Dexter Kozen and Maria-Cristina Patron. Certification of compiler optimizations using Kleene algebra with tests. In John Lloyd, Veronica Dahl, Ulrich Furbach, Manfred Kerber, Kung-Kiu Lau, Catuscia Palamidessi, Luis Moniz Pereira, Yehoshua Sagiv, and Peter J. Stuckey, editors, Proc. 1st Int. Conf. Computational Logic (CL'00), volume 1861 of Lecture Notes in Artificial Intelligence, pages 568-582, London, July 2000. Springer-Verlag.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KP00,
    author="Dexter Kozen and Maria-Cristina Patron",
    title="Certification of compiler optimizations using {K}leene algebra with tests",
    booktitle="Proc. 1st Int. Conf. Computational Logic (CL'00)",
    city="London",
    publisher="Springer-Verlag",
    series="Lecture Notes in Artificial Intelligence",
    volume="1861",
    editor="John Lloyd and Veronica Dahl and Ulrich Furbach and Manfred Kerber and Kung-Kiu Lau and Catuscia Palamidessi and Luis Moniz Pereira and Yehoshua Sagiv and Peter J.~Stuckey",
    address="London",
    month="July",
    year="2000",
    pages="568--582"
  }

  We use Kleene algebra with tests to verify a wide assortment of common compiler optimizations, including dead code elimination, common subexpression elimination, copy propagation, loop hoisting, induction variable elimination, instruction scheduling, algebraic simplification, loop unrolling, elimination of redundant instructions, array bounds check elimination, and introduction of sentinels. In each of these cases, we give a formal equational proof of the correctness of the optimizing transformation.

• Dexter Kozen and Jerzy Tiuryn. On the completeness of propositional Hoare logic. In J. Desharnais, editor, Proc. 5th Int. Seminar Relational Methods in Computer Science (RelMiCS'00), pages 195-202, January 2000. (Subsumed by Dexter Kozen and Jerzy Tiuryn. On the completeness of propositional Hoare logic. Information Sciences, 139(3-4):187-195, 2001.)
  [bibtex] []

  @inproceedings{KT00a,
    author="Dexter Kozen and Jerzy Tiuryn",
    title="On the completeness of propositional {H}oare logic",
    booktitle="Proc. 5th Int. Seminar Relational Methods in Computer Science (RelMiCS'00)",
    editor="J. Desharnais",
    city="Quebec, Canada",
    month="January",
    year="2000",
    pages="195--202"
  }

• Dexter Kozen. On Hoare logic and Kleene algebra with tests. Trans. Computational Logic, 1(1):60-76, July 2000.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K00a,
    author="Dexter Kozen",
    title="On {H}oare logic and {K}leene algebra with tests",
    journal="Trans. Computational Logic",
    volume="1",
    number="1",
    month="July",
    year="2000",
    pages="60--76"
  }

  We show that Kleene algebra with tests (KAT) subsumes propositional Hoare logic (PHL). Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by simple equational reasoning. In addition, we show that all relationally valid inference rules are derivable in KAT and that deciding the relational validity of such rules is PSPACE-complete.

• Dexter Kozen. On Hoare logic and Kleene algebra with tests. In Proc. Conf. Logic in Computer Science (LICS'99), pages 167-172. IEEE, July 1999. (Subsumed by Dexter Kozen. On Hoare logic and Kleene algebra with tests. Trans. Computational Logic, 1(1):60-76, July 2000.)
  [bibtex] []

  @inproceedings{K99c,
    author="Dexter Kozen",
    title="On {H}oare logic and {K}leene algebra with tests",
    booktitle="Proc. Conf. Logic in Computer Science (LICS'99)",
    organization="IEEE",
    city="Trento, Italy",
    month="July",
    year="1999",
    pages="167--172"
  }

• Mark Hopkins and Dexter Kozen. Parikh's theorem in commutative Kleene algebra. In Proc. 14th Conf. Logic in Computer Science (LICS'99), pages 394-401. IEEE, July 1999.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{HK99a,
    author="Mark Hopkins and Dexter Kozen",
    title="Parikh's theorem in commutative {K}leene algebra",
    booktitle="Proc. 14th Conf. Logic in Computer Science (LICS'99)",
    organization="IEEE",
    city="Trento, Italy",
    month="July",
    year="1999",
    pages="394--401"
  }

  Parikh's Theorem says that the commutative image of every context free language is the commutative image of some regular set. Pilling has shown that this theorem is essentially a statement about least solutions of polynomial inequalities. We prove the following general theorem of commutative Kleene algebra, of which Parikh's and Pilling's theorems are special cases: Every system of polynomial inequalities $f_i(x_1,\ldots,x_n) \le x_i$, $1 \le i \le n$, over a commutative Kleene algebra $K$ has a unique least solution in $K^n$; moreover, the components of the solution are given by polynomials in the coefficients of the $f_i$. We also give a closed-form solution in terms of the Jacobian matrix.

• Dexter Kozen. Typed Kleene algebra. Technical Report TR98-1669, Computer Science Department, Cornell University, March 1998.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{K98b,
    author="Dexter Kozen",
    title="Typed {K}leene algebra",
    institution="Computer Science Department, Cornell University",
    number="TR98-1669",
    month="March",
    year="1998"
  }

  In previous work we have found it necessary to argue that certain theorems of Kleene algebra hold even when the symbols are interpreted as nonsquare matrices. In this note we define and investigate typed Kleene algebra, a typed version of Kleene algebra in which objects have types s -> t. Although nonsquare matrices are the principal motivation, there are many other useful interpretations: traces, binary relations, Kleene algebra with tests. We give a set of typing rules and show that every expression has a unique most general typing (mgt). Then we prove the following metatheorem that incorporates the abovementioned results for nonsquare matrices as special cases. Call an expression 1-freeif it contains only the Kleene algebra operators (binary) +, (unary) ⁺, 0, and ·, but no occurrence of 1 or *. Then every universal 1-free formula that is a theorem of Kleene algebra is also a theorem of typed Kleene algebra under its most general typing. The metatheorem is false without the restriction to 1-free formulas.

• Dexter Kozen. Kleene algebra with tests. ACM Trans. Programming Languages and Systems (TOPLAS'97), 19(3):427-443, May 1997. doi:10.1145/256167.256195. (Subsumes Dexter Kozen. Kleene algebra with tests and commutativity conditions. In T. Margaria and B. Steffen, editors, Proc. Second Int. Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), volume 1055 of Lecture Notes in Computer Science, pages 14-33, Passau, Germany, March 1996. Springer-Verlag.)
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K97c,
    title="Kleene algebra with tests",
    author="Dexter Kozen",
    journal="ACM Trans. Programming Languages and Systems (TOPLAS'97)",
    volume="19",
    number="3",
    month="May",
    year="1997",
    pages="427--443",
    doi="10.1145/256167.256195"
  }

  We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program with at most one while loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs. We also show that the universal Horn theory of *-continuous Kleene algebras is not finitely axiomatizable.

• Dexter Kozen. On the complexity of reasoning in Kleene algebra. In Proc. 12th Symp. Logic in Comput. Sci. (LICS'97), pages 195-202, Los Alamitos, Ca., June 1997. IEEE. (Subsumed by Dexter Kozen. On the complexity of reasoning in Kleene algebra. Information and Computation, 179:152-162, 2002.)
  [bibtex] []

  @inproceedings{K97b,
    title="On the complexity of reasoning in {K}leene algebra",
    author="Dexter Kozen",
    booktitle="Proc. 12th Symp. Logic in Comput. Sci. (LICS'97)",
    organization="IEEE",
    address="Los Alamitos, Ca.",
    month="June",
    year="1997",
    pages="195--202"
  }

• Ernie Cohen, Dexter Kozen, and Frederick Smith. The complexity of Kleene algebra with tests. Technical Report TR96-1598, Computer Science Department, Cornell University, July 1996.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{CKS96a,
    author="Ernie Cohen and Dexter Kozen and Frederick Smith",
    title="The complexity of {K}leene algebra with tests",
    institution="Computer Science Department, Cornell University",
    number="TR96-1598",
    month="July",
    year="1996"
  }

  The equational theory of Kleene algebras with tests (KAT) has been shown to be decidable in at most exponential time by an efficient reduction to Propositional Dynamic Logic. We show that the theory is PSPACE-complete. Thus KAT, while considerably more expressive than Kleene algebra, is no more difficult to decide.

• Dexter Kozen and Frederick Smith. Kleene algebra with tests: Completeness and decidability. In D. van Dalen and M. Bezem, editors, Proc. 10th Int. Workshop Computer Science Logic (CSL'96), volume 1258 of Lecture Notes in Computer Science, pages 244-259, Utrecht, The Netherlands, September 1996. Springer-Verlag.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KS96a,
    author="Dexter Kozen and Frederick Smith",
    title="Kleene algebra with tests: Completeness and decidability",
    booktitle="Proc. 10th Int. Workshop Computer Science Logic (CSL'96)",
    editor="D. van Dalen and M. Bezem",
    publisher="Springer-Verlag",
    address="Utrecht, The Netherlands",
    series="Lecture Notes in Computer Science",
    volume="1258",
    month="September",
    year="1996",
    pages="244--259"
  }

  We prove the completeness of the equational theory of Kleene algebra with tests and *-continuous Kleene algebra with tests over language-theoretic and relational models. We also show decidability. Cohen's reduction of Kleene algebra with hypotheses of the form r=0 to Kleene algebra without hypotheses is simplified and extended to handle Kleene algebras with tests.

• Dexter Kozen. Kleene algebra with tests and commutativity conditions. In T. Margaria and B. Steffen, editors, Proc. Second Int. Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96), volume 1055 of Lecture Notes in Computer Science, pages 14-33, Passau, Germany, March 1996. Springer-Verlag. (Subsumed by Dexter Kozen. Kleene algebra with tests. ACM Trans. Programming Languages and Systems (TOPLAS'97), 19(3):427-443, May 1997. doi:10.1145/256167.256195.)
  [full text (.pdf)] [bibtex] []

  @inproceedings{K96b,
    title="Kleene algebra with tests and commutativity conditions",
    author="Dexter Kozen",
    booktitle="Proc. Second Int. Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS'96)",
    month="March",
    year="1996",
    address="Passau, Germany",
    editor="T.~Margaria and B.~Steffen",
    series="Lecture Notes in Computer Science",
    publisher="Springer-Verlag",
    volume="1055",
    pages="14--33"
  }

• Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Infor. and Comput., 110(2):366-390, May 1994.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K94b,
    author="Dexter Kozen",
    title="A completeness theorem for {K}leene algebras and the algebra of regular events",
    journal="Infor. and Comput.",
    volume="110",
    number="2",
    month="May",
    year="1994",
    pages="366--390"
  }

  We give a finitary axiomatization of the algebra of regular events involving only equations and equational implications. Unlike Salomaa's axiomatizations, the axiomatization given here is sound for all interpretations over Kleene algebras.

• Dexter Kozen. Set constraints and logic programming. In J.-P. Jouannaud, editor, Proc. First Conf. Constraints in Computational Logics (CCL'94), volume 845 of Lecture Notes in Computer Science, pages 302-303, Munich, Germany, September 1994. ESPRIT, Springer-Verlag. (Subsumed by Dexter Kozen. Set constraints and logic programming. Information and Computation, 142(1):2-25, April 1998.)
  [bibtex] []

  @inproceedings{K94d,
    title="Set constraints and logic programming",
    author="Dexter Kozen",
    booktitle="Proc. First Conf. Constraints in Computational Logics (CCL'94)",
    organization="ESPRIT",
    month="September",
    year="1994",
    address="Munich, Germany",
    editor="J.-P. Jouannaud",
    series="Lecture Notes in Computer Science",
    publisher="Springer-Verlag",
    volume="845",
    pages="302--303"
  }

• Dexter Kozen. On action algebras. In J. van Eijck and A. Visser, editors, Logic and Information Flow, pages 78-88. MIT Press, 1994.
  [full text (.pdf)] [abstract] [bibtex] []

  @incollection{K92a,
    author="Dexter Kozen",
    title="On action algebras",
    booktitle="Logic and Information Flow",
    pages="78--88",
    year="1994",
    publisher="MIT Press",
    editor="J. van Eijck and A. Visser"
  }

  Action algebras have been proposed by Pratt as an alternative to Kleene algebras. Their chief advantage over Kleene algebras is that they form a finitely-based equational variety, so the essential properties of * (iteration) are captured purely equationally. However, unlike Kleene algebras, they are not closed under the formation of matrices, which renders them inapplicable in certain constructions in automata theory and the design and analysis of algorithms. In this paper we consider a class of action algebras called action lattices. An action lattice is simply an action algebra that forms a lattice under its natural order. Action lattices combine the best features of Kleene algebras and action algebras: like action algebras, they form a finitely-based equational variety; like Kleene algebras, they are closed under the formation of matrices. Moreover, they form the largest subvariety of action algebras for which this is true. All common examples of Kleene algebras appearing in automata theory, logics of programs, relational algebra, and the design and analysis of algorithms are action lattices.

• Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. In Proc. 6th Symp. Logic in Comput. Sci. (LICS'91), pages 214-225, Amsterdam, July 1991. IEEE. (Subsumed by Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Infor. and Comput., 110(2):366-390, May 1994.)
  [bibtex] []

  @inproceedings{K91b,
    author="Dexter Kozen",
    title="A completeness theorem for {K}leene algebras and the algebra of regular events",
    booktitle="Proc. 6th Symp. Logic in Comput. Sci. (LICS'91)",
    organization="IEEE",
    address="Amsterdam",
    pages="214--225",
    month="July",
    year="1991"
  }

• Dexter Kozen and Jerzy Tiuryn. Logics of programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 789-840. North Holland, Amsterdam, 1990.
  [full text (.pdf)] [abstract] [bibtex] []

  @incollection{KT90a,
    title="Logics of Programs",
    author="Dexter Kozen and Jerzy Tiuryn",
    booktitle="Handbook of Theoretical Computer Science",
    volume="B",
    editor="J.~van Leeuwen",
    publisher="North Holland",
    year="1990",
    address="Amsterdam",
    pages="789--840"
  }

  Logics of programs are formal systems for reasoning about computer programs. Traditionally, this has meant formalizing correctness specifications and proving rigorously that those specifications are met by a particular program. Other activities fall into this category as well: determining the equivalence of programs, comparing the expressive power of various operators, synthesing programs from specifications, etc. This chapter gives a brief introduction to some of the basic issues in the study of program logics.

• Dexter Kozen. On Kleene algebras and closed semirings. In Rovan, editor, Proc. Math. Found. Comput. Sci. (MFCS'90), volume 452 of Lecture Notes in Computer Science, pages 26-47, Banska-Bystrica, Slovakia, 1990. Springer-Verlag.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{K90a,
    author="Dexter Kozen",
    title="On {K}leene algebras and closed semirings",
    booktitle="Proc. Math. Found. Comput. Sci. (MFCS'90)",
    editor="Rovan",
    publisher="Springer-Verlag",
    series="Lecture Notes in Computer Science",
    volume="452",
    address="Banska-Bystrica, Slovakia",
    pages="26--47",
    year="1990"
  }

  Kleene algebras are an important class of algebraic structures that arise in diverse areas of computer science: program logic and semantics, relational algebra, automata theory, and the design and analysis of algorithms. The literature contains several inequivalent definitions of Kleene algebras and related algebraic structures. In this paper we establish some new relationships among these structures. Our main results are: (i) There is a Kleene algebra that is not *-continuous. (ii) The categories of *-continuous Kleene algebras, closed semirings, and S-algebras are strongly related by adjunctions. (iii) The axioms of Kleene algebra are not complete for the universal Horn theory of the regular events. This refutes a conjecture of Conway. (iv) Right-handed Kleene algebras are not necessarily left-handed Kleene algebras. This verifies a weaker version of a conjecture of Pratt.

• Neil Immerman and Dexter Kozen. Definability with bounded number of bound variables. Infor. and Comp., 83(2):121-139, November 1989.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{IK89a,
    author="Neil Immerman and Dexter Kozen",
    title="Definability with Bounded Number of Bound Variables",
    journal="Infor. and Comp.",
    volume="83",
    number="2",
    pages="121--139",
    month="November",
    year="1989"
  }

  A theory satisfies the k-variable propertyif every first-order formula is equivalent to a formula with at most k bound variables (possibly reused). Gabbay has shown that a model of temporal logic satisfies the k-variable property for some k if and only if there exists a finite basis for the temporal connectives over that model. We give a model-theoretic method for establishing the k-variable property, involving a restricted Ehrenfeucht-Fraisse game in which each player has only k pebbles. We use the method to unify and simplify results in the literature for linear orders. We also establish new k-variable properties for various theories of bounded-degree trees, and in each case obtain tight upper and lower bounds on k. This gives the first finite basis theorems for branching-time models of temporal logic.

• Dexter Kozen. A finite model theorem for the propositional μ-calculus. Studia Logica, 47(3):233-241, 1988.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K88a,
    author="Dexter Kozen",
    title="A finite model theorem for the propositional $\mu$-calculus",
    journal="Studia Logica",
    volume="47",
    number="3",
    pages="233--241",
    year="1988"
  }

  We prove a finite model theorem and infinitary completeness result for the propositional μ-calculus. The construction establishes a link between finite model theorems for propositional program logics and the theory of well-quasi-orders.

• Neil Immerman and Dexter Kozen. Definability with bounded number of bound variables. In Proc. 2nd Symp. Logic in Comput. Sci. (LICS'87), pages 236-244. IEEE, June 1987. (Subsumed by Neil Immerman and Dexter Kozen. Definability with bounded number of bound variables. Infor. and Comp., 83(2):121-139, November 1989.)
  [bibtex] []

  @inproceedings{IK87a,
    author="Neil Immerman and Dexter Kozen",
    title="Definability with Bounded Number of Bound Variables",
    booktitle="Proc. 2nd Symp. Logic in Comput. Sci. (LICS'87)",
    organization="IEEE",
    pages="236--244",
    month="June",
    year="1987"
  }

• Krzysztof Apt and Dexter Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22:307-309, 1986.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{AK86a,
    author="Krzysztof Apt and Dexter Kozen",
    title="Limits for automatic verification of finite-state concurrent systems",
    journal="Information Processing Letters",
    volume="22",
    pages="307--309",
    year="1986"
  }

  We show that some very simple temporal properties of schematic finite-state programs are not semi-decidable.

• Andreas Blass, Yuri Gurevich, and Dexter Kozen. A zero-one law for logic with a fixed-point operator. Information and Control, 67(1-3):70-90, 1985.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{BGK85,
    author="Andreas Blass and Yuri Gurevich and Dexter Kozen",
    title="A Zero-One Law for Logic with a Fixed-Point Operator",
    journal="Information and Control",
    volume="67",
    number="1-3",
    pages="70--90",
    year="1985"
  }

  The logic obtained by adding the least-fixed-point operator to first-order logic was proposed as a query language by Aho and Ullman (in "Proc. 6th ACM Sympos. on Principles of Programming Languages," 1979, pp. 110-120) and has been studied, particularly in connection with finite models, by numerous authors. We extend to this logic, and to the logic containing the more powerful iterative-fixedpoint operator, the zero-one law proved for first-order logic in (Glebskii, Kogan, Liogonki, and Talanov (1969), Kibernetika 2, 31-42; Fagin (1976), J. Symbolic Logic 41, 50-58). For any sentence $\varphi$ of the extended logic, the proportion of models of $\varphi$ among all structures with universe $\{1,2,\ldots,n\}$ approaches 0 or 1 as $n$ tends to infinity. We also show that the problem of deciding, for any $\varphi$, whether this proportion approaches 1 is complete for exponential time, if we consider only $\varphi$'s with a fixed finite vocabulary (or vocabularies of bounded arity) and complete for double-exponential time if $\varphi$ is unrestricted. In addition, we establish some related results.

• Dexter Kozen. A probabilistic PDL. J. Comput. Syst. Sci., 30(2):162-178, April 1985. (Subsumes Dexter Kozen. A probabilistic PDL. In Proc. 15th Symp. Theory of Comput., pages 291-297. ACM, April 1983.)
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K85a,
    author="Dexter Kozen",
    title="A probabilistic {{\em PDL}}",
    journal="J. Comput. Syst. Sci.",
    volume="30",
    number="2",
    pages="162--178",
    month="April",
    year="1985"
  }

  In this paper we give a probabilistic analog PPDL of Propositional Dynamic Logic. We prove a small model property and give a polynomial space decision procedure for formulas involving well-structured programs. We also give a deductive calculus and illustrate its use by calculating the expected running time of a simple random walk.

• Nissim Francez and Dexter Kozen. Generalized fair termination. In Proc. 11th Symp. Principles of Programming Languages (POPL'84), pages 46-53, Salt Lake City, January 1984. ACM.
  [bibtex] []

  @inproceedings{FK84a,
    author="Nissim Francez and Dexter Kozen",
    title="Generalized fair termination",
    booktitle="Proc. 11th Symp. Principles of Programming Languages (POPL'84)",
    organization="ACM",
    address="Salt Lake City",
    pages="46--53",
    month="January",
    year="1984"
  }

• Edmund Clarke and Dexter Kozen, editors. Proc. Workshop on Logics of Programs 1983, volume 164 of Lecture Notes in Computer Science. Springer-Verlag, 1983. 528 pages.
  [bibtex] []

  @book{K83c,
    title="Proc. Workshop on Logics of Programs 1983",
    editor="Edmund Clarke and Dexter Kozen",
    publisher="Springer-Verlag",
    series="Lecture Notes in Computer Science",
    volume="164",
    year="1983",
    note="528 pages"
  }

• Dexter Kozen. A probabilistic PDL. In Proc. 15th Symp. Theory of Comput., pages 291-297. ACM, April 1983. (Subsumed by Dexter Kozen. A probabilistic PDL. J. Comput. Syst. Sci., 30(2):162-178, April 1985.)
  [bibtex] []

  @inproceedings{K83b,
    author="Dexter Kozen",
    title="A probabilistic {{\em PDL}}",
    booktitle="Proc. 15th Symp. Theory of Comput.",
    organization="ACM",
    pages="291--297",
    month="April",
    year="1983"
  }

• Dexter Kozen. Results on the propositional μ-calculus. Theor. Comput. Sci., 27:333-354, 1983. (Subsumes Dexter Kozen. Results on the propositional μ-calculus. In Proc. 9th Int. Colloq. Automata, Languages, and Programming, pages 348-359, Aarhus, Denmark, July 1982. EATCS.)
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K83a,
    author="Dexter Kozen",
    title="Results on the propositional $\mu$-calculus",
    journal="Theor. Comput. Sci.",
    volume="27",
    pages="333--354",
    year="1983"
  }

  In this paper we define and study a propositional μ-calculus Lμ, which consists essentially of propositional modal logic with a least fixpoint operator. Lμ is syntactically simpler yet strictly more expressive than Propositional Dynamic Logic (PDL). For a restricted version, we give an exponential-time decision procedure, small model property, and complete deductive system, thereby subsuming the corresponding results for PDL.

• Dexter Kozen and Rohit Parikh. A decision procedure for the propositional μ-calculus. In Clarke and Kozen, editors, Proc. Workshop on Logics of Programs, volume 164 of Lecture Notes in Computer Science, pages 313-325. Springer-Verlag, 1983.
  [bibtex] []

  @inproceedings{KP83a,
    author="Dexter Kozen and Rohit Parikh",
    title="A decision procedure for the propositional $\mu$-calculus",
    booktitle="Proc. Workshop on Logics of Programs",
    publisher="Springer-Verlag",
    series="Lecture Notes in Computer Science",
    volume="164",
    editor="Clarke and Kozen",
    pages="313--325",
    year="1983"
  }

• Dexter Kozen, editor. Proc. Workshop on Logics of Programs 1981, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, 1982. 429 pages.
  [bibtex] []

  @book{K82b,
    title="Proc. Workshop on Logics of Programs 1981",
    editor="Dexter Kozen",
    publisher="Springer-Verlag",
    series="Lecture Notes in Computer Science",
    volume="131",
    year="1982",
    note="429 pages"
  }

• Dexter Kozen. Results on the propositional μ-calculus. In Proc. 9th Int. Colloq. Automata, Languages, and Programming, pages 348-359, Aarhus, Denmark, July 1982. EATCS. (Subsumed by Dexter Kozen. Results on the propositional μ-calculus. Theor. Comput. Sci., 27:333-354, 1983.)
  [bibtex] []

  @inproceedings{K82a,
    author="Dexter Kozen",
    title="Results on the propositional $\mu$-calculus",
    booktitle="Proc. 9th Int. Colloq. Automata, Languages, and Programming",
    organization="EATCS",
    address="Aarhus, Denmark",
    pages="348--359",
    month="July",
    year="1982"
  }

• David Harel, Dexter Kozen, and Rohit Parikh. Process logic: Expressiveness, decidability, completeness. J. Comput. Syst. Sci., 25(2):144-170, 1982. (Subsumes David Harel, Dexter Kozen, and Rohit Parikh. Process logic: Expressiveness, decidability, completeness. In Proc. 21st Symp. Found. Comput. Sci., pages 129-142. IEEE, October 1980.)
  [bibtex] []

  @article{HKP82a,
    author="David Harel and Dexter Kozen and Rohit Parikh",
    title="Process logic: Expressiveness, decidability, completeness",
    journal="J. Comput. Syst. Sci.",
    volume="25",
    number="2",
    pages="144--170",
    year="1982"
  }

• Dexter Kozen and Rohit Parikh. An elementary proof of the completeness of PDL. Theor. Comput. Sci., 14(1):113-118, 1981.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KP81a,
    author="Dexter Kozen and Rohit Parikh",
    title="An elementary proof of the completeness of {{\em PDL}}",
    journal="Theor. Comput. Sci.",
    volume="14",
    number="1",
    pages="113--118",
    year="1981"
  }

  We give an elementary proof of the completeness of the Segerberg axioms for Propositional Dynamic Logic.

• Dexter Kozen. Logics of programs. Lecture notes, Aarhus University, Denmark, 1981.
  [bibtex] []

  @unpublished{K81e,
    author="Dexter Kozen",
    title="Logics of Programs",
    note="Lecture notes, Aarhus University, Denmark",
    year="1981"
  }

• Dexter Kozen. On the expressiveness of μ. Manuscript, 1981.
  [bibtex] []

  @unpublished{K81d,
    author="Dexter Kozen",
    title="On the expressiveness of $\mu$",
    year="1981",
    note="Manuscript"
  }

• Dexter Kozen. Positive first-order logic is NP-complete. IBM J. Res. Develop., 25(4):327-332, July 1981.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K81b,
    author="Dexter Kozen",
    title="Positive first-order logic is {{\em NP}}-complete",
    journal="IBM J. Res. Develop.",
    volume="25",
    number="4",
    pages="327--332",
    month="July",
    year="1981"
  }

  Techniques developed in the study of the complexity of finitely presented algebras are used to show that the problem of deciding validity of positive sentences in the language of first-order predicate logic with equality is NP-complete.

• Dexter Kozen. On induction vs. *-continuity. In Kozen, editor, Proc. Workshop on Logic of Programs, volume 131 of Lecture Notes in Computer Science, pages 167-176, New York, 1981. Springer-Verlag.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{K81a,
    author="Dexter Kozen",
    title="On induction vs. *-continuity",
    booktitle="Proc. Workshop on Logic of Programs",
    publisher="Springer-Verlag",
    address="New York",
    series="Lecture Notes in Computer Science",
    volume="131",
    editor="Kozen",
    pages="167--176",
    year="1981"
  }

  In this paper we study the relative expressibility of the infinitary *-continuity condition
  (*-cont)   ${\lt}\alpha^*{\gt} X \equiv \bigvee_n {\lt}\alpha^n{\gt} X$
  and the equational but weaker induction axiom
  (Ind)   $X \wedge [\alpha^*](X \Rightarrow [\alpha]X) \equiv [\alpha^*]X$
  in Propositional Dynamic Logic. We show: (1) under Ind only, there is a first-order sentence distinguishing separable dynamic algebras from standard Kripke models; whereas (2) under the stronger axiom *-cont, the class of separable dynamic algebras and the class of standard Kripke models are indistinguishable by any sentence of infinitary first-order logic.

• David Harel, Dexter Kozen, and Rohit Parikh. Process logic: Expressiveness, decidability, completeness. In Proc. 21st Symp. Found. Comput. Sci., pages 129-142. IEEE, October 1980. (Subsumed by David Harel, Dexter Kozen, and Rohit Parikh. Process logic: Expressiveness, decidability, completeness. J. Comput. Syst. Sci., 25(2):144-170, 1982.)
  [bibtex] []

  @inproceedings{HKP80a,
    author="David Harel and Dexter Kozen and Rohit Parikh",
    title="Process logic: Expressiveness, decidability, completeness",
    booktitle="Proc. 21st Symp. Found. Comput. Sci.",
    organization="IEEE",
    pages="129--142",
    month="October",
    year="1980"
  }

• Dexter Kozen. A representation theorem for models of *-free PDL. In Proc. 7th Colloq. Automata, Languages, and Programming, pages 351-362. EATCS, July 1980.
  [bibtex] []

  @inproceedings{K80b,
    author="Dexter Kozen",
    title="A representation theorem for models of *-free {{\em PDL}}",
    booktitle="Proc. 7th Colloq. Automata, Languages, and Programming",
    organization="EATCS",
    pages="351--362",
    month="July",
    year="1980"
  }

• Dexter Kozen. On the representation of dynamic algebras II. Technical Report RC8290, IBM Thomas J. Watson Research Center, May 1980.
  [bibtex] []

  @techreport{K80a,
    author="Dexter Kozen",
    title="On the representation of dynamic algebras {II}",
    institution="IBM Thomas J. Watson Research Center",
    number="RC8290",
    month="May",
    year="1980"
  }

• Dexter Kozen. Dynamic algebra. In E. Engeler, editor, Proc. Workshop on Logic of Programs, volume 125 of Lecture Notes in Computer Science, pages 102-144. Springer-Verlag, 1979. chapter of Propositional dynamic logics of programs: A survey by Rohit Parikh.
  [bibtex] []

  @inproceedings{K79e,
    author="Dexter Kozen",
    title="Dynamic algebra",
    note="chapter of {\em Propositional dynamic logics of programs: A survey} by Rohit Parikh",
    booktitle="Proc. Workshop on Logic of Programs",
    publisher="Springer-Verlag",
    series="Lecture Notes in Computer Science",
    volume="125",
    editor="E. Engeler",
    pages="102--144",
    year="1979"
  }

• Dexter Kozen. On the duality of dynamic algebras and Kripke models. In E. Engeler, editor, Proc. Workshop on Logic of Programs, volume 125 of Lecture Notes in Computer Science, pages 1-11. Springer-Verlag, 1979.
  [bibtex] []

  @inproceedings{K79d,
    author="Dexter Kozen",
    title="On the duality of dynamic algebras and {K}ripke models",
    booktitle="Proc. Workshop on Logic of Programs",
    publisher="Springer-Verlag",
    series="Lecture Notes in Computer Science",
    volume="125",
    editor="E. Engeler",
    pages="1--11",
    year="1979"
  }

• Dexter Kozen. On the representation of dynamic algebras. Technical Report RC7898, IBM Thomas J. Watson Research Center, October 1979.
  [bibtex] []

  @techreport{K79b,
    author="Dexter Kozen",
    title="On the representation of dynamic algebras",
    institution="IBM Thomas J. Watson Research Center",
    number="RC7898",
    month="October",
    year="1979"
  }

---

Programming Languages & Program Analysis

• Jan Rooduijn, Alexandra Silva, and Dexter Kozen. A cyclic proof system for guarded Kleene algebra with tests. In Christoph Benzmüller, Marijn Heule, and Renate A. Schmidt, editors, Automated Reasoning 12th Int. Joint Conference (IJCAR 2024), volume 14739. Springer LNCS, July 2024.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{RSK24a,
    author="Jan Rooduijn and Alexandra Silva and Dexter Kozen",
    title="A cyclic proof system for guarded {K}leene algebra with tests",
    month="July",
    year="2024",
    booktitle="Automated Reasoning 12th Int. Joint Conference (IJCAR 2024)",
    editor="Christoph Benzmüller and Marijn Heule and Renate A. Schmidt",
    city="Nancy, France",
    publisher="Springer LNCS",
    volume="14739"
  }

  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 makes ordinary sequents sufficient for achieving regular completeness, unlike the situation with Kleene Algebra, where hypersequents are required. Moreover, the proof search induces a co-NP decision procedure, rather than one in PSPACE.

• Dexter Kozen and Alexandra Silva. Multisets and distributions. In Venanzio Capretta, Robbert Krebbers, and Freek Wiedijk, editors, Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday, volume 14560, pages 168-187. Springer LNCS, May 2024.
  [full text] [abstract] [bibtex] []

  @inproceedings{KS24a,
    author="Dexter Kozen and Alexandra Silva",
    title="Multisets and Distributions",
    month="May",
    year="2024",
    booktitle="Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday",
    editor="Venanzio Capretta and Robbert Krebbers and Freek Wiedijk",
    publisher="Springer LNCS",
    volume="14560",
    pages="168--187"
  }

  We give a lightweight alternative construction of Jacobs's distributive law for multisets and distributions that does not involve any combinatorics. We first give a distributive law for lists and distributions, then apply a general theorem on 2-categories that allows properties of lists to be transferred automatically to multisets. The theorem states that equations between 2-cells are preserved by epic 2-natural transformations. In our application, the appropriate epic 2-natural transformation is defined in terms of the Parikh map, familiar from formal language theory, that takes a list to its multiset of elements.

• Dexter Kozen, Alexandra Silva, and Erik Voogd. Joint distributions in probabilistic semantics. In Proc. 39th Conf. Mathematical Foundations of Programming Semantics (MFPS XXXIX), Bloomington, Indiana, June 2023.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KSV23a,
    author="Dexter Kozen and Alexandra Silva and Erik Voogd",
    title="Joint Distributions in Probabilistic Semantics",
    booktitle="Proc. 39th Conf. Mathematical Foundations of Programming Semantics (MFPS XXXIX)",
    address="Bloomington, Indiana",
    month="June",
    year="2023"
  }

  Various categories have been proposed as targets for the denotational semantics of higher-order probabilistic programming languages. One such proposal involves joint probability distributions (couplings) used in Bayesian statistical models with conditioning. In previous treatments, composition of joint measures was performed by disintegrating to obtain Markov kernels, composing the kernels, then reintegrating to obtain a joint measure. Disintegrations exist only under certain restrictions on the underlying spaces. In this paper we propose a category whose morphisms are joint finite measures in which composition is defined without reference to disintegration, allowing its application to a broader class of spaces. The category is symmetric monoidal with a pleasing symmetry in which the dagger structure is a simple transpose.

• Dexter Kozen and Matvey Soloviev. Coalgebraic tools for randomness-conserving protocols. J. Logical and Algebraic Methods in Programming, 125:100734, February 2022. doi:10.1016/j.jlamp.2021.100734. (Subsumes Dexter Kozen and Matvey Soloviev. Coalgebraic tools for randomness-conserving protocols. In J. Desharnais, W. Guttmann, and S. Joosten, editors, Relational and Algebraic Methods in Computer Science (RAMiCS 2018), volume 11194 of LNCS, pages 298-313. Springer, October 2018.)
  [full text] [abstract] [bibtex] []

  @article{KS21a,
    author="Dexter Kozen and Matvey Soloviev",
    title="Coalgebraic Tools for Randomness-Conserving Protocols",
    month="February",
    year="2022",
    journal="J. Logical and Algebraic Methods in Programming",
    volume="125",
    pages="100734",
    doi="10.1016/j.jlamp.2021.100734"
  }

  We propose a coalgebraic model for constructing and reasoning about state-based protocols that implement efficient reductions among random processes. We provide basic tools that allow efficient protocols to be constructed in a compositional way and analyzed in terms of the tradeoff between state and loss of entropy. We show how to use these tools to construct various entropy-conserving reductions between processes.

• Pedro Amorim, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Michael Roberts. Universal semantics for the stochastic lambda-calculus. In Proc. 36th Symp. Logic in Computer Science (LICS'21). ACM/IEEE, June-July 2021.
  [full text] [abstract] [bibtex] []

  @inproceedings{AKMPR21a,
    author="Pedro Amorim and Dexter Kozen and Radu Mardare and Prakash Panangaden and Michael Roberts",
    title="Universal Semantics for the Stochastic Lambda-Calculus",
    booktitle="Proc. 36th Symp. Logic in Computer Science (LICS'21)",
    organization="ACM/IEEE",
    month="June-July",
    year="2021"
  }

  We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used similar techniques to reason about higher-order probabilistic programs, but for the first time admit an adequacy theorem relating the operational and denotational views. This resolves the main issue left open in (Bacci et al. 2018).

• Fredrik Dahlqvist, Alexandra Silva, and Dexter Kozen. Semantics of Probabilistic Programming: A Gentle Introduction, pages 1-42. Cambridge University Press, 2020. URL: https://www.cambridge.org/core/books/foundations-of-probabilistic-programming/819623B1B5B33836476618AC0621F0EE?fbclid=IwAR1ts3WbnRgIO3RJr4V5x3xAk5vsX1rgJqoWjkODHUasUNG6auL1XX5BFLM#, doi:10.1017/9781108770750.002.
  [bibtex] []

  @inbook{DSK20a,
    author="Fredrik Dahlqvist and Alexandra Silva and Dexter Kozen",
    title="Semantics of Probabilistic Programming: A Gentle Introduction",
    booktitle="Foundations of Probabilistic Programming",
    publisher="Cambridge University Press",
    year="2020",
    pages="1--42",
    doi="10.1017/9781108770750.002",
    url="{https://www.cambridge.org/core/books/foundations-of-probabilistic-programming/819623B1B5B33836476618AC0621F0EE?fbclid=IwAR1ts3WbnRgIO3RJr4V5x3xAk5vsX1rgJqoWjkODHUasUNG6auL1XX5BFLM#}"
  }

• Fredrik Dahlqvist and Dexter Kozen. Semantics of higher-order probabilistic programs with conditioning. In Proc. 47th ACM SIGPLAN Symp. Principles of Programming Languages (POPL'20), pages 57:1-29, New Orleans, January 2020. ACM. (Extended version: Fredrik Dahlqvist and Dexter Kozen. Semantics of higher-order probabilistic programs with conditioning. Technical Report http://arxiv.org/abs/1902.11189, Cornell University, February 2019.)
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{DK20a,
    author="Fredrik Dahlqvist and Dexter Kozen",
    title="Semantics of higher-order probabilistic programs with conditioning",
    booktitle="Proc. 47th ACM SIGPLAN Symp. Principles of Programming Languages (POPL'20)",
    organization="ACM",
    pages="57:1--29",
    address="New Orleans",
    month="January",
    year="2020"
  }

  We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the well-known semantics of higher-order programs à la Scott through the use of ordered Banach spaces which allow definitions in terms of fixed points. Our semantics is a model of intuitionistic linear logic: it is based on a symmetric monoidal closed category of ordered Banach spaces which treats randomness as a linear resource, but by constructing an exponential comonad we can also accommodate non-linear reasoning. We apply our semantics to the verification of the classical Gibbs sampling algorithm.

• Steffen Smolka, Praveen Kumar, David Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva. Scalable verification of probabilistic networks. In Programming Language Design and Implementation (PLDI'19), pages 190-203, June 2019.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{SKFHKKS19a,
    author="Steffen Smolka and Praveen Kumar and David Kahn and Nate Foster and Justin Hsu and Dexter Kozen and Alexandra Silva",
    title="Scalable Verification of Probabilistic Networks",
    booktitle="Programming Language Design and Implementation (PLDI'19)",
    city="Phoenix",
    month="June",
    year="2019",
    pages="190--203"
  }

  This paper presents McNetKAT, a scalable tool for verifying probabilistic network programs. McNetKAT is based on a new semantics for the history-free fragment of Probabilistic NetKAT in terms of finite state, absorbing Markov chains. This view allows the semantics of all programs to be computed exactly, enabling construction of an automatic verification tool. Domain-specific optimizations and a parallelizing backend enable McNetKAT to analyze networks with thousands of nodes, automatically reasoning about general properties such as probabilistic program equivalence and refinement, as well as networking properties such as resilience to failures. We evaluate McNetKAT’s scalability using real-world topologies, compare its performance against state-of-the art tools, and develop an extended case study on a recently proposed data center network design.

• Fredrik Dahlqvist and Dexter Kozen. Semantics of higher-order probabilistic programs with conditioning. Technical Report http://arxiv.org/abs/1902.11189, Cornell University, February 2019. (Extended version of: Fredrik Dahlqvist and Dexter Kozen. Semantics of higher-order probabilistic programs with conditioning. In Proc. 47th ACM SIGPLAN Symp. Principles of Programming Languages (POPL'20), pages 57:1-29, New Orleans, January 2020. ACM.)
  [full text] [abstract] [bibtex] []

  @techreport{DK19a,
    author="Fredrik Dahlqvist and Dexter Kozen",
    title="Semantics of higher-order probabilistic programs with conditioning",
    institution="Cornell University",
    number="{\url{http://arxiv.org/abs/1902.11189}}",
    month="February",
    year="2019"
  }

  We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the well-known semantics of higher-order programs a la Scott through the use ordered Banach spaces, which allow definitions in terms of fixed points. Being based on a monoidal rather than cartesian closed structure, our semantics effectively treats randomness as a resource.

• Dexter Kozen. Natural transformations as rewrite rules and monad composition. Logical Methods in Computer Science, 15(1):1-12, January 2019. doi:10.23638/LMCS-15(1:1)2019.
  [full text] [abstract] [bibtex] []

  @article{K19a,
    author="Dexter Kozen",
    title="Natural Transformations as Rewrite Rules and Monad Composition",
    journal="Logical Methods in Computer Science",
    volume="15",
    number="1",
    month="January",
    year="2019",
    pages="1--12",
    doi="10.23638/LMCS-15(1:1)2019"
  }

  Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a different approach involving string rewriting. We show that a given tuple $(T,\mu,\eta)$ is a monad if and only if $T$ is a terminal object in a certain category of strings and rewrite rules, and that this fact can be established by proving confluence of the rewrite system. We illustrate the technique on the monad composition problem. We also give a characterization of adjunctions in terms of rewrite categories.

• Steffen Smolka, Praveen Kumar, Nate Foster, Justin Hsu, David Kahn, Dexter Kozen, and Alexandra Silva. Probabilistic program equivalence for NetKAT. Technical Report http://arxiv.org/abs/1707.02772v2, Cornell University, March 2018.
  [full text] [abstract] [bibtex] []

  @techreport{SKFHKKS18a,
    author="Steffen Smolka and Praveen Kumar and Nate Foster and Justin Hsu and David Kahn and Dexter Kozen and Alexandra Silva",
    title="Probabilistic Program Equivalence for {NetKAT}",
    institution="Cornell University",
    number="{\url{http://arxiv.org/abs/1707.02772v2}}",
    month="March",
    year="2018"
  }

  We tackle the problem of deciding whether two probabilistic programs are equivalent in Probabilistic NetKAT, a formal language for specifying and reasoning about the behavior of packet-switched networks. We show that the problem is decidable for the history-free fragment of the language by developing an effective decision procedure based on stochastic matrices. The main challenge lies in reasoning about iteration, which we address by designing an encoding of the program semantics as a finite-state absorbing Markov chain, whose limiting distribution can be computed exactly. In an extended case study on a real-world data center network, we automatically verify various quantitative properties of interest, including resilience in the presence of failures, by analyzing the Markov chain semantics.

• Dexter Kozen and Francisco Mota. Borel coalgebra and non-wellfounded logic. In Proc. 27th Conf. Math. Found. Programming Semantics (MFPS XXXIII), Ljubljana, Slovenia, June 2017. Elsevier Electronic Notes in Theoretical Computer Science.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KM17a,
    author="Dexter Kozen and Francisco Mota",
    title="Borel Coalgebra and Non-Wellfounded Logic",
    booktitle="Proc. 27th Conf. Math. Found. Programming Semantics (MFPS XXXIII)",
    month="June",
    year="2017",
    address="Ljubljana, Slovenia",
    publisher="Elsevier Electronic Notes in Theoretical Computer Science"
  }

  We introduce Borel coalgebras and Borel automata as a computational approach to basic descriptive set theory. We show that over any Polish space, Borel automata accept exactly the coanalytic sets, and total Borel automata (those that halt on all inputs) accept exactly the Borel sets. The latter result is a computational version of the Kleene-Suslin theorem. The ordinal rank of a Borel set is characterized as the running time of a Borel automaton. We show how these ideas lead to a general notion of non-wellfounded logic in which syntactic objects such as terms and formulas are elements of a final coalgebra. We relate these notions to the categorical theory of recursion schemes (Adamek, Milius, and Velebil 2006, Milius and Moss 2006) to provide a foundation for non-wellfounded logic.

• Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. CoCaml: Functional programming with regular coinductive types. Fundamenta Informaticae, 150:347-377, 2017. doi:10.3233/FI-2017-1473.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{JKS17a,
    author="Jean-Baptiste Jeannin and Dexter Kozen and Alexandra Silva",
    title="{CoCaml}: Functional Programming with Regular Coinductive Types",
    journal="Fundamenta Informaticae",
    volume="150",
    year="2017",
    pages="347--377",
    doi="10.3233/FI-2017-1473"
  }

  Functional languages offer a high level of abstraction, which results in programs that are elegant and easy to understand. Central to the development of functional programming are inductive and coinductive types and associated programming constructs, such as pattern-matching. Whereas inductive types have a long tradition and are well supported in most languages, coinductive types are subject of more recent research and are less mainstream. We present CoCaml, a functional programming language extending OCaml, which allows us to define recursive functions on regular coinductive datatypes. These functions are defined like usual recursive functions, but parameterized by an equation solver. We present a full implementation of all the constructs and solvers and show how these can be used in a variety of examples, including operations on infinite lists, infinitary $\lambda$-terms, and $p$-adic numbers.

• Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. Cantor meets Scott: Domain-theoretic foundations for probabilistic network programming. In Proc. 44th ACM SIGPLAN Symp. Principles of Programming Languages (POPL'17), pages 557-571, Paris, France, January 2017. ACM. doi:10.1145/3009837.3009843.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{SKFKS17a,
    author="Steffen Smolka and Praveen Kumar and Nate Foster and Dexter Kozen and Alexandra Silva",
    title="Cantor meets {S}cott: Domain-Theoretic Foundations for Probabilistic Network Programming",
    booktitle="Proc. 44th ACM SIGPLAN Symp. Principles of Programming Languages (POPL'17)",
    organization="ACM",
    pages="557--571",
    address="Paris, France",
    month="January",
    year="2017",
    doi="10.1145/3009837.3009843"
  }

  ProbNetKAT is a probabilistic extension of NetKAT with a denotational semantics based on Markov kernels. The language is expressive enough to generate continuous distributions, which raises the question of how to compute effectively in the language. This paper gives an new characterization of ProbNetKAT’s semantics using domain theory, which provides the foundation needed to build a practical implementation. We show how to use the semantics to approximate the behavior of arbitrary ProbNetKAT programs using distributions with finite support. We develop a prototype implementation and show how to use it to solve a variety of problems including characterizing the expected congestion induced by different routing schemes and reasoning probabilistically about reachability in a network.

• Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. Cantor meets Scott: Domain-theoretic foundations for probabilistic network programming. Technical Report http://arxiv.org/abs/1607.05830, Cornell University, 20 July 2016. (Subsumed by Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. Cantor meets Scott: Domain-theoretic foundations for probabilistic network programming. In Proc. 44th ACM SIGPLAN Symp. Principles of Programming Languages (POPL'17), pages 557-571, Paris, France, January 2017. ACM. doi:10.1145/3009837.3009843.)
  [full text] [abstract] [bibtex] []

  @techreport{SKFKS16a,
    author="Steffen Smolka and Praveen Kumar and Nate Foster and Dexter Kozen and Alexandra Silva",
    title="Cantor meets {S}cott: Domain-Theoretic Foundations for Probabilistic Network Programming",
    institution="Cornell University",
    number="{\url{http://arxiv.org/abs/1607.05830}}",
    month="20 July",
    year="2016"
  }

  ProbNetKAT is a probabilistic extension of NetKAT with a denotational semantics based on Markov kernels. The language is expressive enough to generate continuous distributions, which raises the question of how to effectively compute in the language. This paper gives an alternative characterization of ProbNetKAT's semantics using domain theory, which provides the foundations needed to build a practical implementation. The new semantics demonstrates that it is possible to analyze ProbNetKAT programs precisely using approximations of fixpoints and distributions with finite support. We develop an implementation and show how to solve a variety of practical problems including characterizing the expected performance of traffic engineering schemes based on randomized routing and reasoning probabilistically about properties such as loop freedom.

• Dexter Kozen. Kolmogorov extension, martingale convergence, and compositionality of processes. In N. Shankar, editor, Proc. 31st ACM-IEEE Symp. Logic in Computer Science (LICS 2016), pages 692-699, New York City, July 2016. ACM.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{K16a,
    author="Dexter Kozen",
    title="Kolmogorov Extension, Martingale Convergence, and Compositionality of Processes",
    booktitle="Proc. 31st ACM-IEEE Symp. Logic in Computer Science (LICS 2016)",
    pages="692--699",
    editor="N.~Shankar",
    publisher="ACM",
    address="New York City",
    month="July",
    year="2016"
  }

  We show that the Kolmogorov extension theorem and the Doob martingale convergence theorem are two aspects of a common generalization, namely a colimit-like construction in a category of Radon spaces and reversible Markov kernels. The construction provides a compositional denotational semantics for standard iteration operators in probabilistic programming languages, e.g. Kleene star or while loops, as a limit of finite approximants, even in the absence of a natural partial order.

• Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic NetKAT. In Peter Thiemann, editor, 25th European Symposium on Programming (ESOP 2016), volume 9632 of Lecture Notes in Computer Science, pages 282-309, Eindhoven, The Netherlands, April 2016. Springer. doi:10.1007/978-3-662-49498-1_12.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{FKMRS15a,
    author="Nate Foster and Dexter Kozen and Konstantinos Mamouras and Mark Reitblatt and Alexandra Silva",
    title="Probabilistic {NetKAT}",
    booktitle="25th European Symposium on Programming (ESOP 2016)",
    editor="Peter Thiemann",
    publisher="Springer",
    series="Lecture Notes in Computer Science",
    volume="9632",
    address="Eindhoven, The Netherlands",
    month="April",
    year="2016",
    pages="282--309",
    doi="10.1007/978-3-662-49498-1_12"
  }

  This paper develops a new language for programming software-defined networks based on a probabilistic semantics. We extend the NetKAT language with new primitives for expressing probabilistic behaviors and enrich the semantics from one based on deterministic functions to one based on measures and measurable functions on sets of packet histories. We establish fundamental properties of the semantics, prove that it is a conservative extension of the deterministic semantics, and show that it satisfies a number of natural equations. We present case studies that show how the language can be used to model a diverse collection of scenarios drawn from real-world networks.

• Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Well-founded coalgebras, revisited. Mathematical Structures in Computer Science, FirstView:1-21, February 2016. doi:10.1017/S0960129515000481.
  [journal link] [full text (.pdf)] [abstract] [bibtex] []

  @article{JKS16a,
    author="Jean-Baptiste Jeannin and Dexter Kozen and Alexandra Silva",
    title="Well-Founded Coalgebras, Revisited",
    journal="Mathematical Structures in Computer Science",
    volume="FirstView",
    month="February",
    year="2016",
    pages="1--21",
    numpages="21",
    issn="1469-8072",
    doi="10.1017/S0960129515000481"
  }

  Theoretical models of recursion schemes have been well studied under the names well-founded coalgebras, recursive coalgebras, corecursive algebras and Elgot algebras. Much of this work focuses on conditions ensuring unique or canonical solutions, e.g. when the coalgebra is well founded. If the coalgebra is not well founded, then there can be multiple solutions. The standard semantics of recursive programs gives a particular solution, typically the least fixpoint of a certain monotone map on a domain whose least element is the totally undefined function; but this solution may not be the desired one. We have recently proposed programming language constructs to allow the specification of alternative solutions and methods to compute them. We have implemented these new constructs as an extension of OCaml. In this paper, we prove some theoretical results characterizing well-founded coalgebras, along with several examples for which this extension is useful. We also give several examples that are not well founded but still have a desired solution. In each case, the function would diverge under the standard semantics of recursion, but can be specified and computed with the programming language constructs we have proposed.

• Carolyn Jane Anderson, Nate Foster, Arjun Guha, Jean-Baptiste Jeannin, Dexter Kozen, Cole Schlesinger, and David Walker. NetKAT: Semantic foundations for networks. In Proc. 41st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL'14), pages 113-126, San Diego, California, USA, January 2014. ACM.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{AFGJKSW13a,
    author="Carolyn Jane Anderson and Nate Foster and Arjun Guha and Jean-Baptiste Jeannin and Dexter Kozen and Cole Schlesinger and David Walker",
    title="{NetKAT}: Semantic Foundations for Networks",
    booktitle="Proc. 41st ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL'14)",
    organization="ACM",
    pages="113--126",
    address="San Diego, California, USA",
    month="January",
    year="2014"
  }

  Recent years have seen growing interest in high-level languages for programming networks. But the design of these languages has been largely ad hoc, driven more by the needs of applications and the capabilities of network hardware than by foundational principles. The lack of a semantic foundation has left language designers with little guidance in determining how to incorporate new features, and programmers without a means to reason precisely about their code. This paper presents NetKAT, a new network programming language that is based on a solid mathematical foundation and comes equipped with a sound and complete equational theory. We describe the design of NetKAT, including primitives for filtering, modifying, and transmitting packets; operators for combining programs in parallel and in sequence; and a Kleene star operator for iteration. We show that NetKAT is an instance of a canonical and well studied mathematical structure called a Kleene algebra with tests (KAT) and prove that its equational theory is sound and complete with respect to its denotational semantics. Finally, we present practical applications of the equational theory including syntactic techniques for checking reachability properties, proving the correctness of compilation and optimization algorithms, and establishing a non-interference property that ensures isolation between programs.

• Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Well-founded coalgebras, revisited. Technical Report http://hdl.handle.net/1813/33330, Computing and Information Science, Cornell University, May 2013. (Subsumed by Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Well-founded coalgebras, revisited. Mathematical Structures in Computer Science, FirstView:1-21, February 2016. doi:10.1017/S0960129515000481.)
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{JKS13b,
    author="Jean-Baptiste Jeannin and Dexter Kozen and Alexandra Silva",
    title="Well-Founded Coalgebras, Revisited",
    institution="Computing and Information Science, Cornell University",
    number="{\url{http://hdl.handle.net/1813/33330}}",
    month="May",
    year="2013"
  }

  Theoretical models of recursion schemes have been well studied under the names well-founded coalgebras, recursive coalgebras, corecursive algebras, and Elgot algebras. Much of this work focuses on conditions ensuring unique or canonical solutions, e.g. when the coalgebra is well-founded. If the coalgebra is not well-founded, then there can be multiple solutions. The standard semantics of recursive programs gives a particular solution, namely the least solution in a flat Scott domain, which may not be the desired one. We have recently proposed programming language constructs to allow the specification of alternative solutions and methods to compute them. We have implemented these new constructs as an extension of OCaml. In this paper, we prove some theoretical results characterizing well-founded coalgebras that slightly extend results of Adámek, Lücke, and Milius (2007), along with several examples for which this extension is useful. We also give several examples that are not well-founded but still have a desired solution. In each case, the function would diverge under the standard semantics of recursion, but can be specified and computed with the programming language constructs we have proposed.

• Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. Language constructs for non-well-founded computation. In Matthias Felleisen and Philippa Gardner, editors, 22nd European Symposium on Programming (ESOP 2013), volume 7792 of Lecture Notes in Computer Science, pages 61-80, Rome, Italy, March 2013. Springer.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{JKS13a,
    author="Jean-Baptiste Jeannin and Dexter Kozen and Alexandra Silva",
    title="Language Constructs for Non-Well-Founded Computation",
    booktitle="22nd European Symposium on Programming (ESOP 2013)",
    editor="Matthias Felleisen and Philippa Gardner",
    month="March",
    year="2013",
    address="Rome, Italy",
    publisher="Springer",
    series="Lecture Notes in Computer Science",
    volume="7792",
    pages="61--80"
  }

  Recursive functions defined on a coalgebraic datatype may not converge if there are cycles in the input, that is, if the input object is not well-founded. Even so, there is often a useful solution. Unfortunately, current functional programming languages provide no support for specifying alternative solution methods. In this paper we give numerous examples in which it would be useful to do so: free variables, α-conversion, and substitution in infinitary λ-terms; halting probabilities and expected running times of probabilistic protocols; abstract interpretation; and constructions involving finite automata. In each case the function would diverge under the standard semantics of recursion. We propose programming language constructs that would allow the specification of alternative solutions and methods to compute them.

• Jean-Baptiste Jeannin and Dexter Kozen. Computing with capsules. J. Automata, Languages and Combinatorics, 17(2-4):185-204, 2012. (Subsumes Jean-Baptiste Jeannin and Dexter Kozen. Computing with capsules. In Martin Kutrib, Nelma Moreira, and Rogério Reis, editors, Proc. Conf. Descriptional Complexity of Formal Systems (DCFS 2012), volume 7386 of Lecture Notes in Computer Science, pages 1-19, Braga, Portugal, July 2012. Springer.)
  [full text (.pdf)] [abstract] [bibtex] []

  @article{JK12b,
    author="Jean-Baptiste Jeannin and Dexter Kozen",
    title="Computing with Capsules",
    journal="J. Automata, Languages and Combinatorics",
    year="2012",
    volume="17",
    number="2--4",
    pages="185--204"
  }

  Capsules provide an algebraic representation of the state of a computation in higher-order functional and imperative languages. A capsule is essentially a finite coalgebraic representation of a regular closed λ-coterm. One can give an operational semantics based on capsules for a higher-order programming language with functional and imperative features, including mutable bindings. Static (lexical) scoping is captured purely algebraically without stacks, heaps, or closures. All operations of interest are typable with simple types, yet the language is Turing complete. Recursive functions are represented directly as capsules without the need for fixpoint combinators.

• Jean-Baptiste Jeannin and Dexter Kozen. Computing with capsules. In Martin Kutrib, Nelma Moreira, and Rogério Reis, editors, Proc. Conf. Descriptional Complexity of Formal Systems (DCFS 2012), volume 7386 of Lecture Notes in Computer Science, pages 1-19, Braga, Portugal, July 2012. Springer. (Subsumed by Jean-Baptiste Jeannin and Dexter Kozen. Computing with capsules. J. Automata, Languages and Combinatorics, 17(2-4):185-204, 2012.)
  [bibtex] []

  @inproceedings{JK11a,
    author="Jean-Baptiste Jeannin and Dexter Kozen",
    title="Computing with Capsules",
    booktitle="Proc. Conf. Descriptional Complexity of Formal Systems (DCFS 2012)",
    editor="Martin Kutrib and Nelma Moreira and Rog{\'e}rio Reis",
    month="July",
    year="2012",
    address="Braga, Portugal",
    publisher="Springer",
    series="Lecture Notes in Computer Science",
    volume="7386",
    pages="1--19"
  }

• Dexter Kozen. Realization of coinductive types. In Michael Mislove and Joël Ouaknine, editors, Proc. 27th Conf. Math. Found. Programming Semantics (MFPS XXVII), pages 148-155, Pittsburgh, PA, May 2011. Elsevier Electronic Notes in Theoretical Computer Science.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{K11a,
    author="Dexter Kozen",
    title="Realization of Coinductive Types",
    booktitle="Proc. 27th Conf. Math. Found. Programming Semantics (MFPS XXVII)",
    editor="Michael Mislove and Jo{\"e}l Ouaknine",
    month="May",
    year="2011",
    address="Pittsburgh, PA",
    pages="148--155",
    publisher="Elsevier Electronic Notes in Theoretical Computer Science"
  }

  We give an explicit combinatorial construction of final coalgebras for a modest generalization of polynomial functors on Set. Type signatures are modeled as directed multigraphs instead of endofunctors. The final coalgebra for a type signature F involves the notion of Brzozowski derivative on sets of paths in F.

• Dexter Kozen, editor. Science of Computer Programming, volume 65:2. Elsevier, March 2007. Special issue dedicated to selected papers from the 7th Int. Conf. Mathematics of Program Construction (MPC'04).
  [bibtex] []

  @book{K07a,
    title="Science of Computer Programming",
    editor="Dexter Kozen",
    publisher="Elsevier",
    volume="65:2",
    month="March",
    year="2007",
    note="Special issue dedicated to selected papers from the 7th Int. Conf. Mathematics of Program Construction (MPC'04)"
  }

• Łucja Kot and Dexter Kozen. Kleene algebra and bytecode verification. Electronic Notes in Theoretical Computer Science, 141(1):221-236, December 2005.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KK05a,
    author="{\L}ucja Kot and Dexter Kozen",
    title="{K}leene Algebra and Bytecode Verification",
    journal="Electronic Notes in Theoretical Computer Science",
    volume="141",
    number="1",
    month="December",
    year="2005",
    pages="221--236"
  }

  Most standard approaches to the static analysis of programs, such as the popular worklist method, are first-order methods that inductively annotate program points with abstract values. In [6] we introduced a second-order approach based on Kleene algebra. In this approach, the primary objects of interest are not the abstract data values, but the transfer functions that manipulate them. These elements form a left-handed Kleene algebra. The dataflow labeling is not achieved by inductively labeling the program with abstract values, but rather by computing the star (Kleene closure) of a matrix of transfer functions. In this paper we show how this general framework applies to the problem of Java bytecode verification. We show how to specify transfer functions arising in Java bytecode verification in such a way that the Kleene algebra operations (join, composition, star) can be computed efficiently. We also give a hybrid dataflow analysis algorithm that computes the closure of a matrix on a cutset of the control flow graph, thereby avoiding the recalculation of dataflow information when there are cycles in the graph. This method could potentially improve the performance over the standard worklist algorithm when a small cutset can be found.

• Łucja Kot and Dexter Kozen. Kleene algebra and bytecode verification. In Fausto Spoto, editor, Proc. 1st Workshop Bytecode Semantics, Verification, Analysis, and Transformation (Bytecode'05), pages 201-215, April 2005. (Subsumed by Łucja Kot and Dexter Kozen. Kleene algebra and bytecode verification. Electronic Notes in Theoretical Computer Science, 141(1):221-236, December 2005.)
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KK04b,
    author="{\L}ucja Kot and Dexter Kozen",
    title="{K}leene Algebra and Bytecode Verification",
    booktitle="Proc. 1st Workshop Bytecode Semantics, Verification, Analysis, and Transformation (Bytecode'05)",
    editor="Fausto Spoto",
    city="Edinburgh",
    month="April",
    year="2005",
    pages="201--215"
  }

  In this paper we show how the general framework introduced in the paper "Second-Order Abstract Interpretation via Kleene Algebra" applies to the problem of Java bytecode verification. We show how to specify transfer functions arising in Java bytecode verification in such a way that the Kleene algebra operations (join, composition, star) can be computed efficiently. We also give a hybrid dataflow analysis algorithm that computes the closure of a matrix on a cutset of the control flow graph, thereby avoiding the recalculation of dataflow information along long paths. This method could potentially improve the performance over the standard worklist algorithm when a small cutset can be found.

• Łucja Kot and Dexter Kozen. Second-order abstract interpretation via Kleene algebra. Technical Report TR2004-1971, Computer Science Department, Cornell University, December 2004.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{KK04a,
    author="{\L}ucja Kot and Dexter Kozen",
    title="Second-Order Abstract Interpretation via {K}leene Algebra",
    institution="Computer Science Department, Cornell University",
    number="TR2004-1971",
    month="December",
    year="2004"
  }

  Most standard approaches to the static analysis of programs, such as the popular worklist method, are first-order methods that inductively annotate program points with abstract values. In this paper we introduce a second-order approach based on Kleene algebra. In this approach, the primary objects of interest are not the abstract data values, but the transfer functions that manipulate them. These elements form a Kleene algebra. The dataflow labeling is not achieved by inductively labeling the program with abstract values, but rather by computing the star (Kleene closure) of a matrix of transfer functions. In this paper we introduce the method and prove soundness and completeness with respect to the standard worklist algorithm.

• Dexter Kozen, editor. Proc. 7th Int. Conf. Mathematics of Program Construction (MPC 2004), volume 3125 of Lecture Notes in Computer Science. Springer-Verlag, July 2004. 400 pages.
  [bibtex] []

  @book{K04d,
    title="Proc. 7th Int. Conf. Mathematics of Program Construction (MPC 2004)",
    editor="Dexter Kozen",
    publisher="Springer-Verlag",
    series="Lecture Notes in Computer Science",
    city="Stirling, Scotland",
    volume="3125",
    month="July",
    year="2004",
    isbn="3-540-22380-0",
    note="400 pages"
  }

• Dexter Kozen. Kleene algebras with tests and the static analysis of programs. Technical Report TR2003-1915, Computer Science Department, Cornell University, November 2003.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{K03c,
    author="Dexter Kozen",
    title="Kleene Algebras with Tests and the Static Analysis of Programs",
    institution="Computer Science Department, Cornell University",
    number="TR2003-1915",
    month="November",
    year="2003"
  }

  We propose a general framework for the static analysis of programs based on Kleene algebra with tests (KAT). We show how KAT can be used to statically verify compliance with safety policies specified by security automata. We prove soundness and completeness over relational interpretations. We illustrate the method on an example involving the correctness of a device driver.

• Robert Givan, David McAllester, Carl Witty, and Dexter Kozen. Tarskian set constraints. Information and Computation, 174(2):105-131, May 2002.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{GMWK02,
    author="Robert Givan and David McAllester and Carl Witty and Dexter Kozen",
    title="Tarskian Set Constraints",
    journal="Information and Computation",
    volume="174",
    number="2",
    pages="105--131",
    month="May",
    year="2002"
  }

  We investigate set constraints over set expressions with Tarskian functional and relational operations. Unlike the Herbrand constructor symbols used in recent set constraint formalisms, the meaning of a Tarskian function symbol is interpreted in an arbitrary first order structure. We show that satisfiability of Tarskian set constraints is decidable in nondeterministic doubly exponential time. We also give complexity results and open problems for various extensions and restrictions of the language.

• Dexter Kozen and Matt Stillerman. Eager class initialization for Java. In W. Damm and E.R. Olderog, editors, Proc. 7th Int. Symp. Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), volume 2469 of Lecture Notes in Computer Science, pages 71-80. IFIP, Springer-Verlag, Sept. 2002.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KS02a,
    author="Dexter Kozen and Matt Stillerman",
    title="Eager Class Initialization for {J}ava",
    booktitle="Proc. 7th Int. Symp. Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02)",
    organization="IFIP",
    editor="W.~Damm and E.R.~Olderog",
    series="Lecture Notes in Computer Science",
    volume="2469",
    publisher="Springer-Verlag",
    city="Oldenburg, Germany",
    month="Sept.",
    year="2002",
    pages="71--80"
  }

  We describe a static analysis method on Java bytecode to determine class initialization dependencies. This method can be used for eager class loading and initialization. It catches many initialization circularities that are missed by the standard lazy implementation. Except for contrived examples, the computed initialization order gives the same results as standard lazy initialization.

• Dexter Kozen. Set constraints and logic programming. Information and Computation, 142(1):2-25, April 1998.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K95b,
    title="Set constraints and logic programming",
    author="Dexter Kozen",
    journal="Information and Computation",
    volume="142",
    number="1",
    month="April",
    year="1998",
    pages="2--25"
  }

  Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are the main ingredient in set-based program analysis. In this paper we describe a constraint logic programming language CLP(SC) over set constraints in the style of Jaffar and Lassez. The language subsumes ordinary logic programs over an Herbrand domain. We give an efficient unification algorithm and operational, declarative, and fixpoint semantics. We show how the language can be applied in set-based program analysis by deriving explicitly the monadic approximation of the collecting semantics of Heintze and Jaffar.

• Allan Cheng and Dexter Kozen. Some notes on rational spaces. Technical Report TR96-1576, Computer Science Department, Cornell University, March 1996.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{CK96a,
    author="Allan Cheng and Dexter Kozen",
    title="Some notes on rational spaces",
    institution="Computer Science Department, Cornell University",
    number="TR96-1576",
    month="March",
    year="1996"
  }

  Set constraints are inclusions between expressions denoting set of ground terms over a finitely ranked alphabet. Rational spaces are topological spaces obtained as spaces of runs of topological hypergraphs. They were introduced by Kozen, who described the topological structure of spaces of solutions to systems of set constraints in terms of rational spaces. In this paper we continue the investigation of rational spaces. We give a Myhill-Nerode like characterization of rational points, which in turn is used to rederive results about the rational points of finitary rational spaces. We define congruences on hypergraphs and investigate their interplay with the Myhill-Nerode characterization, and determine the computational complexity of some decision problems related to rational spaces.

• Dexter Kozen. Rational spaces and set constraints. Theoretical Computer Science, 167:73-94, 1996.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K96a,
    title="Rational spaces and set constraints",
    author="Dexter Kozen",
    journal="Theoretical Computer Science",
    volume="167",
    year="1996",
    pages="73--94"
  }

  Set constraints are inclusions between expressions denoting sets of ground terms. They have been used extensively in program analysis and type inference. In this paper we investigate the topological structure of the spaces of solutions to systems of set constraints. We identify a family of topological spaces called rational spaces, which formalize the notion of a topological space with a regular or self-similar structure, such as the Cantor discontinuum or the space of runs of a finite automaton. We develop the basic theory of rational spaces and derive generalizations and proofs from topological principles of some results in the literature on set constraints.

• Robert Givan, Dexter Kozen, David McAllester, and Carl Witty. Tarskian set constraints. In Proc. 11th Symp. Logic in Comput. Sci. (LICS'96), pages 138-147, New Brunswick, NJ, July 1996. IEEE. (Subsumed by Robert Givan, David McAllester, Carl Witty, and Dexter Kozen. Tarskian set constraints. Information and Computation, 174(2):105-131, May 2002.)
  [bibtex] []

  @inproceedings{GKMW96,
    author="Robert Givan and Dexter Kozen and David McAllester and Carl Witty",
    title="Tarskian set constraints",
    booktitle="Proc. 11th Symp. Logic in Comput. Sci. (LICS'96)",
    organization="IEEE",
    address="New Brunswick, NJ",
    month="July",
    year="1996",
    pages="138--147"
  }

• Allan Cheng and Dexter Kozen. A complete Gentzen-style axiomatization for set constraints. In F. Meyer auf der Heide and B. Monien, editors, Proc. 23rd Int. Colloq. Automata, Languages, and Programming (ICALP'96), volume 1099 of Lecture Notes in Computer Science, pages 134-145, Paderborn, Germany, July 1996. Eur. Assoc. for Theoretical Comput. Sci., Springer-Verlag.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{CK95,
    author="Allan Cheng and Dexter Kozen",
    title="A complete {G}entzen-style axiomatization for set constraints",
    booktitle="Proc. 23rd Int. Colloq. Automata, Languages, and Programming (ICALP'96)",
    organization="Eur. Assoc. for Theoretical Comput. Sci.",
    month="July",
    year="1996",
    address="Paderborn, Germany",
    editor="F. Meyer auf der Heide and B. Monien",
    series="Lecture Notes in Computer Science",
    publisher="Springer-Verlag",
    volume="1099",
    pages="134--145"
  }

  Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are the main ingredient in set-based program analysis. In this paper we provide a Gentzen-style axiomatization for sequents $P\vdash Q$, where $P$ and $Q$ are finite sets of set constraints, based on the axioms of termset algebra. Sequents of the restricted form $P\vdash \mathit{false}$ correspond to positive set constraints, and those of the more general form $P\vdash Q$ correspond to systems of mixed positive and negative set constraints. We show that the deductive system is (i) complete for the restricted sequents $P\vdash \mathit{false}$ over standard models, (ii) incomplete for general sequents $P\vdash Q$ over standard models, but (iii) complete for general sequents over set-theoretic termset algebras.

• Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5:113-125, 1995.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KPS95a,
    author="Dexter Kozen and Jens Palsberg and Michael I. Schwartzbach",
    title="Efficient recursive subtyping",
    journal="Mathematical Structures in Computer Science",
    volume="5",
    pages="113--125",
    year="1995"
  }

  Subtyping in the presence of recursive types for the lambda-calculus was studied by Amadio and Cardelli in 1991. In that paper they showed that the problem of deciding whether one recursive type is a subtype of another is decidable in exponential time. In this paper we give an $O(n^2)$ algorithm. Our algorithm is based on a simplification of the definition of the subtype relation, which allows us to reduce the problem to the emptiness problem for a certain finite automaton with quadratically many states. It is known that equality of recursive types and the covariant Böhm order can be decided efficiently by means of finite automata, since they are just language equality and language inclusion, respectively. Our results extend the automata-theoretic approach to handle orderings based on contravariance.

• Dexter Kozen. Rational spaces and set constraints. In Peter D. Mosses, Mogens Nielsen, and Michael I. Schwartzbach, editors, Proc. Sixth Int. Joint Conf. Theory and Practice of Software Develop. (TAPSOFT'95), volume 915 of Lecture Notes in Computer Science, pages 42-61, Aarhus, Denmark, May 1995. Springer-Verlag. (Subsumed by Dexter Kozen. Rational spaces and set constraints. Theoretical Computer Science, 167:73-94, 1996.)
  [bibtex] []

  @inproceedings{K95a,
    title="Rational spaces and set constraints",
    author="Dexter Kozen",
    booktitle="Proc. Sixth Int. Joint Conf. Theory and Practice of Software Develop. (TAPSOFT'95)",
    month="May",
    year="1995",
    address="Aarhus, Denmark",
    editor="Peter D. Mosses and Mogens Nielsen and Michael I. Schwartzbach",
    series="Lecture Notes in Computer Science",
    publisher="Springer-Verlag",
    volume="915",
    pages="42--61"
  }

• Alexander Aiken, Dexter Kozen, and Edward Wimmers. Decidability of systems of set constraints with negative constraints. Infor. and Comput., 122(1):30-44, October 1995.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{AKW93a,
    title="Decidability of systems of set constraints with negative constraints",
    author="Alexander Aiken and Dexter Kozen and Edward Wimmers",
    journal="Infor. and Comput.",
    pages="30--44",
    year="1995",
    month="October",
    volume="122",
    number="1"
  }

  Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. Recently, several algorithms for solving general systems of positive set constraints have appeared. In this paper we consider systems of mixed positive and negative constraints, which are considerably more expressive than positive constraints alone. We show that it is decidable whether a given such system has a solution. The proof involves a reduction to a number-theoretic decision problem that may be of independent interest.

• Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient inference of partial types. J. Comput. Syst. Sci., 49(2):306-324, October 1994.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KPS94a,
    author="Dexter Kozen and Jens Palsberg and Michael I. Schwartzbach",
    title="Efficient inference of partial types",
    journal="J. Comput. Syst. Sci.",
    volume="49",
    number="2",
    pages="306--324",
    month="October",
    year="1994"
  }

  Partial types for the lambda-calculus were introduced by Thatte in 1988 as a means of typing objects that are not typable with simple types, such as heterogeneous lists and persistent data. In that paper he showed that type inference for partial types was semidecidable. Decidability remained open until quite recently, when O'Keefe and Wand gave an exponential time algorithm for type inference. In this paper we give an $O(n^3)$ algorithm. Our algorithm constructs a certain finite automaton that represents a canonical solution to a given set of type constraints. Moreover, the construction works equally well for recursive types; this solves an open problem of O'Keefe and Wand.

• Dexter Kozen. Logical aspects of set constraints. In E. Börger, Y. Gurevich, and K. Meinke, editors, Proc. 1993 Conf. Computer Science Logic (CSL'93), volume 832 of Lecture Notes in Computer Science, pages 175-188, Swansea, U. K., September 1993. Eur. Assoc. Comput. Sci. Logic, Springer-Verlag.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{K94a,
    title="Logical aspects of set constraints",
    author="Dexter Kozen",
    booktitle="Proc. 1993 Conf. Computer Science Logic (CSL'93)",
    organization="Eur. Assoc. Comput. Sci. Logic",
    month="September",
    year="1993",
    address="Swansea, U. K.",
    editor="E. B{\"o}rger and Y. Gurevich and K. Meinke",
    series="Lecture Notes in Computer Science",
    publisher="Springer-Verlag",
    volume="832",
    pages="175--188"
  }

  Set constraints are inclusion relations between sets of ground terms over a ranked alphabet. They have been used extensively in program analysis and type inference. Here we present an equational axiomatization of the algebra of set constraints. Models of these axioms are called termset algebras. They are related to the Boolean algebras with operators of Jonsson and Tarski. We also define a family of combinatorial models called topological term automata, which are essentially the term automata studied by Kozen, Palsberg, and Schwartzbach endowed with a topology such that all relevant operations are continuous. These models are similar to Kripke frames for modal or dynamic logic. We establish a Stone duality between termset algebras and topological term automata, and use this to derive a completeness theorem for a related multidimensional modal logic. Finally, we prove a small model property by filtration, and argue that this result contains the essence of several algorithms appearing in the literature on set constraints.

• Alexander Aiken, Dexter Kozen, Moshe Vardi, and Edward Wimmers. The complexity of set constraints. In E. Börger, Y. Gurevich, and K. Meinke, editors, Proc. 1993 Conf. Computer Science Logic (CSL'93), volume 832 of Lecture Notes in Computer Science, pages 1-17, Swansea, U. K., September 1993. Eur. Assoc. Comput. Sci. Logic, Springer-Verlag.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{AKVW93a,
    title="The complexity of set constraints",
    author="Alexander Aiken and Dexter Kozen and Moshe Vardi and Edward Wimmers",
    booktitle="Proc. 1993 Conf. Computer Science Logic (CSL'93)",
    organization="Eur. Assoc. Comput. Sci. Logic",
    month="September",
    year="1993",
    address="Swansea, U. K.",
    editor="E. B{\"o}rger and Y. Gurevich and K. Meinke",
    series="Lecture Notes in Computer Science",
    publisher="Springer-Verlag",
    volume="832",
    pages="1--17"
  }

  Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. We present several results on the computational complexity of solving systems of set constraints. The systems we study form a natural complexity hierarchy depending on the form of the constraint language.

• Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. In Proc. 20th Symp. Princip. Programming Lang. (POPL'93), pages 419-428, Charleston, SC, January 1993. ACM. (Subsumed by Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science, 5:113-125, 1995.)
  [bibtex] []

  @inproceedings{KPS93a,
    author="Dexter Kozen and Jens Palsberg and Michael I. Schwartzbach",
    title="Efficient recursive subtyping",
    booktitle="Proc. 20th Symp. Princip. Programming Lang. (POPL'93)",
    organization="ACM",
    address="Charleston, SC",
    pages="419--428",
    month="January",
    year="1993"
  }

• Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient inference of partial types. In Proc. 33rd Symp. Found. Comput. Sci. (FOCS'92), pages 363-371. IEEE, October 1992. (Subsumed by Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient inference of partial types. J. Comput. Syst. Sci., 49(2):306-324, October 1994.)
  [bibtex] []

  @inproceedings{KPS92a,
    author="Dexter Kozen and Jens Palsberg and Michael I. Schwartzbach",
    title="Efficient inference of partial types",
    booktitle="Proc. 33rd Symp. Found. Comput. Sci. (FOCS'92)",
    organization="IEEE",
    pages="363--371",
    month="October",
    year="1992"
  }

• Wilfred Chen, John Field, Dexter Kozen, William Pugh, Tim Teitelbaum, and Brad Vander Zanden. ALEX-an alexical programming language. In Ichikawa, Jungert, and Korfhage, editors, Visual Languages and Applications, pages 147-158. Plenum Press, 1990.
  [bibtex] []

  @incollection{CFKPTZ90a,
    author="Wilfred Chen and John Field and Dexter Kozen and William Pugh and Tim Teitelbaum and Brad Vander Zanden",
    title="{ALEX}---an alexical programming language",
    booktitle="Visual Languages and Applications",
    editor="Ichikawa and Jungert and Korfhage",
    publisher="Plenum Press",
    pages="147--158",
    year="1990"
  }

• Wilfred Chen, John Field, Dexter Kozen, William Pugh, Tim Teitelbaum, and Brad Vander Zanden. ALEX-an alexical programming language. In Proc. 1987 Workshop on Visual Languages, pages 315-329, Linköping, Sweden, August 1987. (Subsumed by Wilfred Chen, John Field, Dexter Kozen, William Pugh, Tim Teitelbaum, and Brad Vander Zanden. ALEX-an alexical programming language. In Ichikawa, Jungert, and Korfhage, editors, Visual Languages and Applications, pages 147-158. Plenum Press, 1990.)
  [bibtex] []

  @inproceedings{CFKPTZ87a,
    author="Wilfred Chen and John Field and Dexter Kozen and William Pugh and Tim Teitelbaum and Brad Vander Zanden",
    title="{ALEX}---an alexical programming language",
    booktitle="Proc. 1987 Workshop on Visual Languages",
    address="Link{\"o}ping, Sweden",
    pages="315--329",
    month="August",
    year="1987"
  }

• David Harel and Dexter Kozen. A programming language for the inductive sets, and applications. Information and Control, 63(1-2):118-139, 1984. (Subsumes David Harel and Dexter Kozen. A programming language for the inductive sets, and applications. In Proc. 9th Int. Colloq. Automata, Languages, and Programming, pages 313-329, Aarhus, Denmark, July 1982. EATCS.)
  [full text (.pdf)] [abstract] [bibtex] []

  @article{HK84a,
    author="David Harel and Dexter Kozen",
    title="A programming language for the inductive sets, and applications",
    journal="Information and Control",
    volume="63",
    number="1--2",
    pages="118--139",
    year="1984"
  }

  We describe a programming language IND that generalizes alternating Turing machines to arbitrary first-order structures. We show that IND programs (resp. everywhere-halting IND programs, loop-free IND programs) accept precisely the inductively definable (resp. hyperelementary, elementary) relations. We give several examples showing how the language provides a robust and computational approach to the theory of first-order inductive definability. We then show: (1) on all acceptable structures (in the sense of Moschovakis ("Elementary Induction on Abstract Structures," North-Holland, Amsterdam, 1974), r.e. dynamic logic is more expressive than finite-test dynamic logic. This refines a separation result of Meyer and Parikh ("Proc. 12th ACM Sympos. on Theory of Computing," 1979, pp. 167-175); (2) IND provides a natural query language for the set of fixpoint queries over a relational database, answering a question of Chandra and Harel (J. Comput. System Sci. 25, No. 1 (1982), 99 128).

• Corrado Böhm and Dexter Kozen. Eliminating recursion over acyclic data structures in functional programs. In 4th Int. Workshop on the Semantics of Programming Languages, Bull. EATCS, volume 20, page 205, Bad Honnef, June 1983. EATCS.
  [bibtex] []

  @inproceedings{BK83,
    author="Corrado B{\"o}hm and Dexter Kozen",
    title="Eliminating recursion over acyclic data structures in functional programs",
    booktitle="4th Int. Workshop on the Semantics of Programming Languages, Bull. EATCS",
    organization="EATCS",
    volume="20",
    pages="205",
    address="Bad Honnef",
    month="June",
    year="1983"
  }

• David Harel and Dexter Kozen. A programming language for the inductive sets, and applications. In Proc. 9th Int. Colloq. Automata, Languages, and Programming, pages 313-329, Aarhus, Denmark, July 1982. EATCS. (Subsumed by David Harel and Dexter Kozen. A programming language for the inductive sets, and applications. Information and Control, 63(1-2):118-139, 1984.)
  [bibtex] []

  @inproceedings{HK82a,
    author="David Harel and Dexter Kozen",
    title="A programming language for the inductive sets, and applications",
    booktitle="Proc. 9th Int. Colloq. Automata, Languages, and Programming",
    organization="EATCS",
    address="Aarhus, Denmark",
    pages="313--329",
    month="July",
    year="1982"
  }

• Dexter Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22(3):328-350, June 1981. doi:10.1016/0022-0000(81)90036-2. (Subsumes Dexter Kozen. Semantics of probabilistic programs. In Proc. 20th Symp. Found. Comput. Sci., pages 101-114. IEEE, October 1979.)
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K81c,
    author="Dexter Kozen",
    title="Semantics of probabilistic programs",
    journal="J. Comput. Syst. Sci.",
    volume="22",
    number="3",
    pages="328--350",
    month="June",
    year="1981",
    doi="10.1016/0022-0000(81)90036-2"
  }

  This paper presents two complementary but equivalent semantics for a high level probabilistic programming language. One of these interprets programs as partial measurable functions on a measurable space. The other interprets programs as continuous linear operators on a Banach space of measures. It is shown how the ordered domains of Scott and others are embedded naturally into these spaces. We use the semantics to prove a general result about probabilistic programs, namely that a program's behavior is completely determined by its action on fixed inputs.

• Dexter Kozen. Semantics of probabilistic programs. In Proc. 20th Symp. Found. Comput. Sci., pages 101-114. IEEE, October 1979. (Subsumed by Dexter Kozen. Semantics of probabilistic programs. J. Comput. Syst. Sci., 22(3):328-350, June 1981. doi:10.1016/0022-0000(81)90036-2.)
  [bibtex] []

  @inproceedings{K79c,
    author="Dexter Kozen",
    title="Semantics of probabilistic programs",
    booktitle="Proc. 20th Symp. Found. Comput. Sci.",
    organization="IEEE",
    pages="101--114",
    month="October",
    year="1979"
  }

---

Computational Algebra

• Mark Bickford, Dexter Kozen, and Alexandra Silva. Formalizing Moessner’s theorem and generalizations in NUPRL. Journal of Logical and Algebraic Methods in Programming, (JLAMP 100713):1-12, 2021. doi:10.1016/j.jlamp.2021.100713.
  [abstract] [bibtex] []

  @article{BKS21a,
    author="Mark Bickford and Dexter Kozen and Alexandra Silva",
    title="Formalizing {M}oessner’s theorem and generalizations in {NUPRL}",
    journal="Journal of Logical and Algebraic Methods in Programming",
    number="JLAMP 100713",
    year="2021",
    pages="1--12",
    doi="10.1016/j.jlamp.2021.100713",
    year="2021"
  }

  Moessner's theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers $1^n$, $2^n$, $3^n$,... Several generalizations of Moessner's theorem exist. Recently, Kozen and Silva gave an algebraic proof of a general theorem that subsumes Moessner's original theorem and its known generalizations. In this note, we describe the formalization of this theorem that the first author did in NUPRL. On the one hand, the formalization remains remarkably close to the original proof. On the other hand, it leads to new insights in the proof, pointing to small gaps and ambiguities that would never raise any objections in pen and pencil proofs, but which must be resolved in machine formalization.

• Dexter Kozen and Alexandra Silva. On Moessner's theorem. The American Mathematical Monthly, 120(2):131-139, February 2013.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KS13a,
    author="Dexter Kozen and Alexandra Silva",
    title="On {M}oessner's Theorem",
    journal="The American Mathematical Monthly",
    volume="120",
    number="2",
    month="February",
    year="2013",
    pages="131--139",
    publisher="Mathematical Association of America"
  }

  Moessner's theorem describes a procedure for generating a sequence of $n$ integer sequences that lead unexpectedly to the sequence of $n$th powers $1^n$, $2^n$, $3^n$, ...  Paasche's theorem is a generalization of Moessner's; by varying the parameters of the procedure, one can obtain the sequence of factorials $1!$, $2!$, $3!$, ... or the sequence of superfactorials $1!!$, $2!!$, $3!!$, ...  Long's theorem generalizes Moessner's in another direction, providing a procedure to generate the sequence $a1^{n-1}$, $(a+d)2^{n-1}$, $(a+2d)3^{n-1}$, ...  Proofs of these results in the literature are typically based on combinatorics of binomial coefficients or calculational scans. In this note we give a short and revealing algebraic proof of a general theorem that contains Moessner's, Paasche's, and Long's as special cases. We also prove a generalization that gives new Moessner-type theorems.

• Dexter Kozen and Kjartan Stefansson. Computing the Newtonian graph. Journal of Symbolic Computation, 24:125-136, 1997.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KS96b,
    title="Computing the {N}ewtonian graph",
    author="Dexter Kozen and Kjartan Stefansson",
    journal="Journal of Symbolic Computation",
    year="1997",
    volume="24",
    pages="125--136"
  }

  In his study of Newton's root approximation method, Smale defined the Newtonian graph of a complex univariate polynomial $f$. The vertices of this graph are the roots of $f$ and $f'$ and the edges are the degenerate curves of flow of the Newtonian vector field $N_f(z) = -f(z)/f'(z)$. The embedded edges of this graph form the boundaries of root basins in Newton's root approximation method. The graph defines a treelike relation on the roots of $f$ and $f'$, similar to the linear order when $f$ has only real roots. We give an efficient algebraic algorithm based on cell decomposition to compute the Newtonian graph. The resulting structure can be used to query whether two complex points are in the same basin. This suggests a modified version of Newton's method in which one can test whether a step has crossed a basin boundary. We show that this modified version does not necessarily converge to a root. Stefansson has recently extended this algorithm to handle rational and algebraic functions without significant increase in complexity. He has shown that the Newtonian graph tesselates the associated Riemann surface and can be used in conjunction with Euler's formula to give an NC algorithm to calculate the genus of an algebraic curve.

• Dexter Kozen, Susan Landau, and Richard Zippel. Decomposition of algebraic functions. Journal of Symbolic Computation, 22(3):235-246, September 1996.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KLZ96,
    title="Decomposition of Algebraic Functions",
    author="Dexter Kozen and Susan Landau and Richard Zippel",
    journal="Journal of Symbolic Computation",
    volume="22",
    number="3",
    month="September",
    year="1996",
    pages="235--246"
  }

  Functional decomposition---whether a function $f(x)$ can be written as a composition of functions $g(h(x))$ in a nontrivial way---is an important primitive in symbolic computation systems. The problem of univariate polynomial decomposition was shown to have an efficient solution by Kozen and Landau. Dickerson and von zur Gathen gave algorithms for certain multivariate cases. Zippel showed how to decompose rational functions. In this paper, we address the issue of decomposition of algebraic functions. We show that the problem is related to univariate resultants in algebraic function fields, and in fact can be reformulated as a problem of resultant decomposition. We characterize all decompositions of a given algebraic function up to isomorphism, and give an exponential time algorithm for finding a nontrivial one if it exists. The algorithm involves genus calculations and constructing transcendental generators of fields of genus zero.

• Dexter Kozen. Efficient resolution of singularities of plane curves. In P. S. Thiagarajan, editor, Proc. 14th Conf. Foundations of Software Technology and Theoretical Computer Science, volume 880 of Lecture Notes in Computer Science, pages 1-11, Madras, India, December 1994. Springer-Verlag.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{K94c,
    author="Dexter Kozen",
    title="Efficient resolution of singularities of plane curves",
    booktitle="Proc. 14th Conf. Foundations of Software Technology and Theoretical Computer Science",
    editor="P. S. Thiagarajan",
    month="December",
    address="Madras, India",
    year="1994",
    series="Lecture Notes in Computer Science",
    publisher="Springer-Verlag",
    volume="880",
    pages="1--11"
  }

  We give a new algorithm for resolving singularities of plane curves. The algorithm is polynomial time in the bit complexity model, does not require factorization, and works over the rationals or finite fields.

• Jin-Yi Cai, W. H. J. Fuchs, Dexter Kozen, and Zicheng Liu. Efficient average-case algorithms for the modular group. In Proc. 35th Symp. Found. Comput. Sci. (FOCS'94), pages 143-152. IEEE, November 1994.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{CFKL94,
    title="Efficient average-case algorithms for the modular group",
    author="Jin{-}Yi Cai and W. H. J. Fuchs and Dexter Kozen and Zicheng Liu",
    booktitle="Proc. 35th Symp. Found. Comput. Sci. (FOCS'94)",
    organization="IEEE",
    month="November",
    year="1994",
    pages="143--152"
  }

  The modular group occupies a central position in many branches of mathematical sciences. In this paper we give average polynomial-time algorithms for the unbounded and bounded membership problems for finitely generated subgroups of the modular group. The latter result affirms a conjecture of Gurevich.

• Dexter Kozen, Susan Landau, and Richard Zippel. Decomposition of algebraic functions. In L. Adleman and M.-D. Huang, editors, Proc. First Algorithmic Number Theory Symposium (ANTS), volume 877 of Lecture Notes in Computer Science, pages 80-92, Ithaca, New York, May 1994. Mathematical Sciences Institute, Springer-Verlag. (Subsumed by Dexter Kozen, Susan Landau, and Richard Zippel. Decomposition of algebraic functions. Journal of Symbolic Computation, 22(3):235-246, September 1996.)
  [bibtex] []

  @inproceedings{KLZ94a,
    title="Decomposition of algebraic functions",
    author="Dexter Kozen and Susan Landau and Richard Zippel",
    booktitle="Proc. First Algorithmic Number Theory Symposium (ANTS)",
    organization="Mathematical Sciences Institute",
    address="Ithaca, New York",
    month="May",
    year="1994",
    editor="L. Adleman and M.-D. Huang",
    series="Lecture Notes in Computer Science",
    publisher="Springer-Verlag",
    volume="877",
    pages="80--92"
  }

• Doug Ierardi and Dexter Kozen. Parallel resultant computation. In J. Reif, editor, Synthesis of Parallel Algorithms, pages 679-720. Morgan Kaufmann, 1993.
  [full text (.pdf)] [abstract] [bibtex] []

  @incollection{IK93a,
    title="Parallel resultant computation",
    author="Doug Ierardi and Dexter Kozen",
    booktitle="Synthesis of Parallel Algorithms",
    editor="J. Reif",
    publisher="Morgan Kaufmann",
    year="1993",
    pages="679--720"
  }

  This is a survey paper on resultants. From the introduction: A resultant is a purely algebraic criterion for determining whether a finite collection of polynomials have a common zero. It has been shown to be a useful tool in the design of efficient parallel and sequential algorithms in symbolic algebra, computational geometry, computational number theory, and robotics. We begin with a brief history of resultants and a discussion of some of their important applications. Next we review some of the mathematical background in commutative algebra that will be used in subsequent sections. The Nullstellensatz of Hilbert is presented in both its strong and weak forms. We also discuss briefly the necessary background on graded algebras, and define affine and projective spaces over arbitrary fields. We next present a detailed account of the resultant of a pair of univariate polynomials, and present efficient parallel algorithms for its computation. The theory of subresultants is developed in detail, and the computation of polynomial remainder sequences is derived. A resultant system for several univariate polynomials and algorithms for the gcd of several polynomials are given. Finally, we develop the theory of multivariate resultants as a natural extension of the univariate case. Here we treat both classical results on the projective (homogeneous) case, as well as more recent results on the affine (inhomogeneous) case. The u-resultantof a set of multivariate polynomials is defined and a parallel algorithm is presented. We discuss the computation of generalized characteristic polynomials and relate them to the decision problem for the theories of real closed and algebraically closed fields.

• Dexter Kozen and Susan Landau. Polynomial decomposition algorithms. J. Symb. Comput., 7:445-456, 1989.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KL89a,
    author="Dexter Kozen and Susan Landau",
    title="Polynomial decomposition algorithms",
    journal="J. Symb. Comput.",
    volume="7",
    pages="445--456",
    year="1989"
  }

  We examine the question of when a polynomial $f$ over a commutative ring has a nontrivial functional decomposition $f(x) = g(h(x))$. Previous algorithms (Barton and Zippel 76, Barton and Zippel 85, Alagar and Thahn 85) are exponential-time in the worst case, require polynomial factorization, and only work over fields of characteristic 0. We present an $O(n^2)$-time algorithm. We also show that the problem is in NC. The algorithm does not use polynomial factorization, and works over any commutative ring containing a multiplicative inverse of $r$. Finally, we give a new structure theorem that leads to necessary and sufficient algebraic conditions for decomposibility over any field. We apply this theorem to obtain an NC algorithm for decomposing irreducible polynomials over finite fields, and a subexponential algorithm for decomposing irreducible polynomials over any field admitting efficient polynomial factorization.

• Michael Ben-Or, Ephraim Feig, Dexter Kozen, and Prasoon Tiwari. Fast parallel algorithms for finding the roots of a polynomial with all real roots. SIAM J. Comput., 17(6):1081-1092, 1988. doi:10.1137/0217069.
  [journal link] [abstract] [bibtex] []

  @article{BFKT88a,
    author="Michael Ben-Or and Ephraim Feig and Dexter Kozen and Prasoon Tiwari",
    title="Fast parallel algorithms for finding the roots of a polynomial with all real roots",
    journal="SIAM J. Comput.",
    volume="17",
    number="6",
    pages="1081--1092",
    year="1988",
    doi="10.1137/0217069"
  }

  Given a polynomial $p(z)$ of degree $n$ with $m$ bit integer coefficients and an integer $\mu$, the problem of determining all its roots with error less than $2^\mu$ is considered. It is shown that this problem is in the class NC if $p(z)$ has all real roots. Some very interesting properties of a Sturm sequence of a polynomial with distinct real roots are proved and used in the design of a fast parallel algorithm for this problem. Using Newton identities and a novel numerical integration scheme for evaluating a contour integral to high precision, this algorithm determines good approximations to the linear factors of $p(z)$.

• Joachim von zur Gathen, Dexter Kozen, and Susan Landau. Functional decomposition of polynomials. In Proc. 28th Symp. Foundations of Computer Science (FOCS'87), pages 127-131. IEEE, November 1987.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{GKL87a,
    author="Joachim von zur Gathen and Dexter Kozen and Susan Landau",
    title="Functional decomposition of polynomials",
    booktitle="Proc. 28th Symp. Foundations of Computer Science (FOCS'87)",
    organization="IEEE",
    pages="127--131",
    month="November",
    year="1987"
  }

  This paper deals with the following decomposition problem: given $f$ a polynomial in $F[x]$ of degree $n$, decide whether $f$ has a nontrivial functional decomposition $f = g\circ h$. If so, determine the coefficients of $g$ and $h$. We present fast sequential and parallel algorithms for this problem.

---

Automata & Formal Languages

• Dexter Kozen. Theory of Computation. Springer, New York, 2006.
  [table of contents (.pdf)] [abstract] [bibtex] []

  @book{K06a,
    author="Dexter Kozen",
    title="Theory of Computation",
    publisher="Springer",
    address="New York",
    year="2006",
    isbn="10: 1-84628-297-7",
    isbn="13: 978-1-84628-297-3"
  }

  A graduate-level text on theory of computation.

• Dexter Kozen. Automata on guarded strings and applications. Matématica Contemporânea, 24:117-139, 2003.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K03a,
    author="Dexter Kozen",
    title="Automata on Guarded Strings and Applications",
    journal="Mat{\'e}matica Contempor{\^a}nea",
    volume="24",
    year="2003",
    pages="117--139"
  }

  Guarded strings are like ordinary strings over a finite alphabet P, except that atoms of the free Boolean algebra on a set of atomic tests B alternate with the symbols of P. The regular sets of guarded strings play the same role in Kleene algebra with tests as the regular sets of ordinary strings do in Kleene algebra. In this paper we develop the elementary theory of finite automata on guarded strings, a generalization of the theory of finite automata on ordinary strings. We give several basic constructions, including determinization, state minimization, and an analog of Kleene's theorem. We then use these results to verify a conjecture on the complexity of a complete Gentzen-style sequent calculus for partial correctness. We also show that a basic result of the theory of Boolean decision diagrams (BDDs), namely that minimal ordered BDDs are unique, is a special case of the Myhill-Nerode theorem for a class of automata on guarded strings.

• Dexter Kozen. On two letters versus three. In Zoltán Ésik and Anna Ingólfsdóttir, editors, Proc. Workshop on Fixed Points in Computer Science (FICS'02), pages 44-50, July 2002.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{K02a,
    author="Dexter Kozen",
    title="On Two Letters versus Three",
    booktitle="Proc. Workshop on Fixed Points in Computer Science (FICS'02)",
    city="Copenhagen",
    editor="Zolt{\'a}n {\'E}sik and Anna Ing{\'o}lfsd{\'o}ttir",
    month="July",
    year="2002",
    pages="44--50"
  }

  If A is a context-free language over a two-letter alphabet, then the set of all words obtained by sorting words in A and the set of all permutations of words in A are context-free. This is false over alphabets of three or more letters. Thus these problems illustrate a difference in behavior between two- and three-letter alphabets.

• Hubert Comon, Dexter Kozen, Helmut Seidl, and Moshe Y. Vardi, editors. Applications of Tree Automata in Rewriting, Logic, and Programming, number 9743 in Dagstuhl Seminar Reports, October 1997.
  [bibtex] []

  @proceedings{CKSV97,
    editor="Hubert Comon and Dexter Kozen and Helmut Seidl and Moshe Y.~Vardi",
    title="Applications of Tree Automata in Rewriting, Logic, and Programming",
    series="Dagstuhl Seminar Reports",
    number="9743",
    month="October",
    year="1997"
  }

• Dexter Kozen. Automata and Computability. Springer-Verlag, New York, 1997.
  [table of contents (.pdf)] [abstract] [bibtex] []

  @book{K97a,
    title="Automata and Computability",
    author="Dexter Kozen",
    publisher="Springer-Verlag",
    address="New York",
    year="1997",
    isbn="0-387-94907-0"
  }

  An undergraduate text on automata and computability theory.

• Dexter Kozen. On regularity-preserving functions. Bull. Europ. Assoc. Theor. Comput. Sci., 58:131-138, February 1996.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K95c,
    author="Dexter Kozen",
    title="On regularity-preserving functions",
    journal="Bull. Europ. Assoc. Theor. Comput. Sci.",
    volume="58",
    pages="131--138",
    month="February",
    year="1996"
  }

  A characterization of numeric functions that preserve regularity.

• Nils Klarlund and Dexter Kozen. Rabin measures. Chicago Journal of Theoretical Computer Science, 1995(3), September 1995.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KK95a,
    author="Nils Klarlund and Dexter Kozen",
    title="Rabin Measures",
    journal="Chicago Journal of Theoretical Computer Science",
    volume="1995",
    number="3",
    publisher="MIT Press",
    month="September",
    year="1995"
  }

  Rabin conditions are a general class of properties of infinite sequences that encompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper, we introduce a concept, called a Rabin measure, which in a precise sense expresses progress for each transition towards satisfaction of the Rabin condition. We show that these measures of progress are linked to the Kleene-Brouwer ordering of recursion theory. Klarlund uses this property to establish an exponential upper bound for the complementation of automata on infinite trees. When applied to termination problems under fairness constraints, Rabin measures eliminate the need for syntax-dependent, recursive applications of proof rules.

• Dexter Kozen. Partial automata and finitely generated congruences: An extension of Nerode's theorem. In J. N. Crossley, J. B. Remmel, R. A. Shore, and M. E. Sweedler, editors, Logical Methods: In Honor of Anil Nerode's Sixtieth Birthday, pages 490-511. Birkhäuser, Ithaca, New York, 1993.
  [full text (.pdf)] [abstract] [bibtex] []

  @incollection{K92c,
    author="Dexter Kozen",
    title="Partial automata and finitely generated congruences: An extension of {N}erode's theorem",
    booktitle="Logical Methods: In Honor of Anil Nerode's Sixtieth Birthday",
    editor="J. N. Crossley and J. B. Remmel and R. A. Shore and M. E. Sweedler",
    address="Ithaca, New York",
    pages="490--511",
    publisher="Birkh{\"a}user",
    year="1993"
  }

  Let T be the set of ground terms over a finite ranked alphabet. We define partial automata on T and prove that the finitely generated congruences on T are in one-to-one correspondence (up to isomorphism) with the finite partial automata on T with no inaccessible and no inessential states. We give an application in term rewriting: every ground term rewrite system has a canonical equivalent system that can be constructed in polynomial time.

• Dexter Kozen. On the Myhill-Nerode theorem for trees. Bull. Europ. Assoc. Theor. Comput. Sci., 47:170-173, June 1992.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{K92b,
    author="Dexter Kozen",
    title="On the {M}yhill-{N}erode theorem for trees",
    journal="Bull. Europ. Assoc. Theor. Comput. Sci.",
    volume="47",
    pages="170--173",
    month="June",
    year="1992"
  }

  We present an elementary proof of the Myhill-Nerode Theorem for term automata.

• Nils Klarlund and Dexter Kozen. Rabin measures and their application to fairness and automata theory. In Proc. 6th Symp. Logic in Comput. Sci. (LICS'91), pages 256-265. IEEE, July 1991. (Subsumed by Nils Klarlund and Dexter Kozen. Rabin measures. Chicago Journal of Theoretical Computer Science, 1995(3), September 1995.)
  [bibtex] []

  @inproceedings{KK91a,
    author="Nils Klarlund and Dexter Kozen",
    title="Rabin measures and their application to fairness and automata theory",
    booktitle="Proc. 6th Symp. Logic in Comput. Sci. (LICS'91)",
    organization="IEEE",
    pages="256--265",
    month="July",
    year="1991"
  }

---

Algorithms & Complexity

• Anshuman Mohan, Yunhe Liu, Nate Foster, Tobias Kappé, and Dexter Kozen. Formal abstractions for packet scheduling. Proc. ACM Program. Lang., 7(OOPSLA2):1338-1362, October 2023. Article 269. doi:10.1145/3622845. (Extended version: Anshuman Mohan, Yunhe Liu, Nate Foster, Tobias Kappé, and Dexter Kozen. Formal abstractions for packet scheduling. Technical Report http://arxiv.org/abs/2211.11659, Cornell University, November 2022.)
  [full text] [abstract] [bibtex] []

  @article{MLFKK23a,
    author="Anshuman Mohan and Yunhe Liu and Nate Foster and Tobias Kappé and Dexter Kozen",
    title="Formal Abstractions for Packet Scheduling",
    journal="Proc. ACM Program. Lang.",
    month="October",
    year="2023",
    volume="7",
    number="OOPSLA2",
    doi="10.1145/3622845",
    note="Article 269",
    pages="1338--1362"
  }

  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.

• Anshuman Mohan, Yunhe Liu, Nate Foster, Tobias Kappé, and Dexter Kozen. Formal abstractions for packet scheduling. Technical Report http://arxiv.org/abs/2211.11659, Cornell University, November 2022. (Extended version of: Anshuman Mohan, Yunhe Liu, Nate Foster, Tobias Kappé, and Dexter Kozen. Formal abstractions for packet scheduling. Proc. ACM Program. Lang., 7(OOPSLA2):1338-1362, October 2023. Article 269. doi:10.1145/3622845.)
  [full text] [abstract] [bibtex] []

  @techreport{MLFKK22a,
    author="Anshuman Mohan and Yunhe Liu and Nate Foster and Tobias Kappé and Dexter Kozen",
    title="Formal Abstractions for Packet Scheduling",
    month="November",
    year="2022",
    institution="Cornell University",
    number="{\url{http://arxiv.org/abs/2211.11659}}"
  }

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

• Dexter Kozen. Optimal coin flipping. In F. van Breugel et al., editor, Panangaden Festschrift, volume 8464 of Lecture Notes in Computer Science, pages 407-426. Springer, May 2014.
  [full text (.pdf)] [abstract] [bibtex] []

  @incollection{K14a,
    author="Dexter Kozen",
    title="Optimal Coin Flipping",
    booktitle="Panangaden Festschrift",
    editor="F.~van Breugel et al.",
    series="Lecture Notes in Computer Science",
    volume="8464",
    publisher="Springer",
    pages="407--426",
    month="May",
    year="2014"
  }

  This paper studies the problem of simulating a coin of arbitrary real bias $q$ with a coin of arbitrary real bias $p$ with minimum loss of entropy. We establish a lower bound that is strictly greater than the information-theoretic bound. We show that as a function of $q$, it is an everywhere-discontinuous self-similar fractal. We provide efficient protocols that achieve the lower bound to within any desired accuracy for $(3-\sqrt 5)/2 < p < 1/2$ and achieve it exactly for $p=1/2$.

• Nikos Karampatziakis and Dexter Kozen. Learning prediction suffix trees with Winnow. In Léon Bottou and Michael Littman, editors, Proc. 26th Int. Conf. Machine Learning (ICML'09), pages 489-496, Montreal, Canada, June 2009. Omnipress.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KK09a,
    author="Nikos Karampatziakis and Dexter Kozen",
    title="Learning Prediction Suffix Trees with {Winnow}",
    booktitle="Proc. 26th Int. Conf. Machine Learning (ICML'09)",
    address="Montreal, Canada",
    month="June",
    year="2009",
    pages="489--496",
    editor="L\'{e}on Bottou and Michael Littman",
    publisher="Omnipress"
  }

  Prediction suffix trees (PSTs) are a popular tool for modeling sequences and have been successfully applied in many domains such as compression and language modeling. In this work we adapt the well studied Winnow algorithm to the task of learning PSTs. The proposed algorithm automatically grows the tree, so that it provably remains competitive with any fixed PST determined in hindsight. At the same time we prove that the depth of the tree grows only logarithmically with the number of mistakes made by the algorithm. Finally, we empirically demonstrate its effectiveness in two different tasks.

• Dexter Kozen. Lexicographic flow. Technical Report http://hdl.handle.net/1813/13018, Computing and Information Science, Cornell University, June 2009.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{K09b,
    author="Dexter Kozen",
    title="Lexicographic Flow",
    institution="Computing and Information Science, Cornell University",
    number="{\url{http://hdl.handle.net/1813/13018}}",
    month="June",
    year="2009"
  }

  The lexicographic flow problem is a flow problem in which the edges are assigned priorities, and we wish to find a flow that is lexicographically maximum with respect to the priority assignment. The problem is reducible to a weighted flow problem, but we show that exponentially large weights are necessary in general. We then give an efficient direct algorithm that does not use weights.

• Carla Marceau and Dexter Kozen. AppMon: Application monitors for not-yet-trusted software. Technical Report TR07-0005, Odyssey Research Associates, June 2007.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{MK07,
    author="Carla Marceau and Dexter Kozen",
    title="{AppMon}: Application Monitors for Not-Yet-Trusted Software",
    institution="Odyssey Research Associates",
    number="TR07-0005",
    month="June",
    year="2007"
  }

  AppMon represents a novel approach to monitoring the behavior of not-yet-trusted applications that avoids the disadvantages of current approaches. It is based on a self-customizing monitor that constrains the application's use of computer resources. A self-customizing monitor learns how the application normally uses computer resources and does not interfere with normal use. However, when the application uses resources in an unusual way, AppMon prevents potentially harmful accesses. Self-customizing monitors satisfy three important requirements on application security monitors. First, the application can be run immediately without testing or training. Second, customization is automatic, so only minimal demands are made on the user and system administrator. Finally, the self-customizing monitors are applicable to a wide variety of applications, including those that read and write files, read and write registry keys, invoke other processes, and use the Internet.

• Dexter Kozen and Alexa Sharp. On distance coloring. Technical Report TR2007-2084, Computing and Information Science, Cornell University, June 2007.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{KS07a,
    author="Dexter Kozen and Alexa Sharp",
    title="On Distance Coloring",
    institution="Computing and Information Science, Cornell University",
    number="TR2007-2084",
    month="June",
    year="2007"
  }

  Call a connected undirected graph (d,c)-colorable if there is a vertex coloring using at most c colors such that no two vertices of distance d or less have the same color. It is well known that (1,2)-colorability is decidable in linear time, but (1,c)-colorability for c >= 3 is NP-complete. Sharp (2007) shows that for fixed d >= 2, the (d,c)-colorability problem is solvable in linear time for c <= 3d/2 and NP-complete otherwise. In this note we give an alternative construction that improves the upper time bound as a function of d for the case c <= 3d/2. The construction entails a generalization of the notion of tree ecomposition and bounded treewidth (Robertson and Seymour 1986) to arbitrary overlay graphs, not just trees, which may be of independent interest.

• Daniel Sheldon, M. A. Saleh Elmohamed, and Dexter Kozen. Collective inference on Markov models for modeling bird migration. In J. Platt, D. Koller, Y. Singer, and S. Roweis, editors, Advances in Neural Information Processing Systems (NIPS'07), volume 20, December 2007.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{SEK07a,
    author="Daniel Sheldon and M. A. Saleh Elmohamed and Dexter Kozen",
    title="Collective Inference on {M}arkov Models for Modeling Bird Migration",
    booktitle="Advances in Neural Information Processing Systems (NIPS'07)",
    volume="20",
    editor="J. Platt and D. Koller and Y. Singer and S. Roweis",
    city="Vancouver, BC, Canada",
    month="December",
    year="2007"
  }

  We investigate a family of inference problems on Markov models, where many sample paths are drawn from a Markov chain and partial information is revealed to an observer who attempts to reconstruct the sample paths. We present algorithms and hardness results for several variants of this problem which arise by revealing different information to the observer and imposing different requirements for the reconstruction of sample paths. Our algorithms are analogous to the classical Viterbi algorithm for Hidden Markov Models, which finds single most probable sample path given a sequence of observations. Our work is motivated by an important application in ecology: inferring bird migration paths from a large database of observations.

• Dexter Kozen, Yaron Minsky, and Brian Smith. Efficient algorithms for optimal video transmission. In James A. Storer and Martin Cohn, editors, Proc. Data Compression Conference (DCC'98), pages 229-238, Snowbird, Utah, March 1998. IEEE.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KMS98,
    author="Dexter Kozen and Yaron Minsky and Brian Smith",
    title="Efficient algorithms for optimal video transmission",
    booktitle="Proc. Data Compression Conference (DCC'98)",
    organization="IEEE",
    editor="James A. Storer and Martin Cohn",
    address="Snowbird, Utah",
    month="March",
    year="1998",
    pages="229--238"
  }

  This paper addresses the problem of sending an encoded video stream over a channel of limited bandwidth. When there is insufficient bandwidth available, some data must be dropped. For many video encodings, some data are more important that others, leading to a natural prioritization of the data. In this paper we give fast algorithms to determine a prioritization which optimizes the visual quality of the received data. By optimized visual quality, we mean that the expected maximum interval of unplayable frames is minimized. Our results are obtained in a model of encoded video data that is applicable to many encoding technologies. The highlight of the model is an interesting relationship between the play order and dependence order of frames. The property allows fast determination of optimal send orders by dynamic programming and is satisfied by all MPEG sequences.

• Dexter Kozen and Shmuel Zaks. Optimal bounds for the change-making problem. Theor. Comput. Sci., 123:377-388, 1994.
  [full text (.pdf)] [abstract] [bibtex] []

  @article{KZ94,
    author="Dexter Kozen and Shmuel Zaks",
    title="Optimal bounds for the change-making problem",
    journal="Theor. Comput. Sci.",
    volume="123",
    pages="377--388",
    year="1994"
  }

  The change-making problem is the problem of representing a given value with the fewest coins possible. We investigate the problem of determining whether the greedy algorithm produces an optimal representation of all amounts for a given set of coin denominations $1 = c_1 < c_2 < \cdots < c_m$. Chang and Gill show that if the greedy algorithm is not always optimal, then there exists a counterexample $x$ in the range \[c_3 \le x \lt (c_m(c_mc_{m-1} + c_m - 3c_{m-1}) / (c_m - c_{m-1}).\] To test for the existence of such a counterexample, Chang and Gill propose computing and comparing the greedy and optimal representations of all $x$ in this range. In this paper we show that if a counterexample exists, then the smallest one lies in the range \[c_3 + 1 < x < c_m + c_{m-1},\] and these bounds are tight. Moreover, we give a simple test for the existence of a counterexample that does not require the calculation of optimal representations. In addition, we give a complete characterization of three-coin systems and an efficient algorithm for all systems with a fixed number of coins. Finally, we show that a related problem is coNP-complete.

• Dexter Kozen and Kjartan Stefánsson. Computing the Newtonian graph. In Trans. 11th Army Conference on Applied Math. and Computing, pages 55-69. Army Research Office, June 1993. (Subsumed by Dexter Kozen and Kjartan Stefansson. Computing the Newtonian graph. Journal of Symbolic Computation, 24:125-136, 1997.)
  [bibtex] []

  @inproceedings{KS93a,
    title="Computing the {N}ewtonian graph",
    author="Dexter Kozen and Kjartan Stef{\'a}nsson",
    booktitle="Trans. 11th Army Conference on Applied Math. and Computing",
    organization="Army Research Office",
    month="June",
    year="1993",
    pages="55--69"
  }

• Dexter Kozen and Shmuel Zaks. Optimal bounds for the change-making problem. In Proc. 20th Int. Colloq. on Automata, Languages, and Programming (ICALP'93), volume 700 of Lecture Notes in Computer Science, pages 150-161, Lund, Sweden, July 1993. EATCS, Springer-Verlag. (Subsumed by Dexter Kozen and Shmuel Zaks. Optimal bounds for the change-making problem. Theor. Comput. Sci., 123:377-388, 1994.)
  [bibtex] []

  @inproceedings{KZ93a,
    author="Dexter Kozen and Shmuel Zaks",
    title="Optimal bounds for the change-making problem",
    booktitle="Proc. 20th Int. Colloq. on Automata, Languages, and Programming (ICALP'93)",
    organization="EATCS",
    address="Lund, Sweden",
    series="Lecture Notes in Computer Science",
    publisher="Springer-Verlag",
    volume="700",
    pages="150--161",
    month="July",
    year="1993"
  }

• Joachim von zur Gathen, Marek Karpinski, and Dexter Kozen, editors. Algebraic Complexity and Parallelism, number 9230 in Dagstuhl Seminar Reports, July 1992.
  [bibtex] []

  @proceedings{GKK92,
    editor="Joachim von zur Gathen and Marek Karpinski and Dexter Kozen",
    title="Algebraic Complexity and Parallelism",
    series="Dagstuhl Seminar Reports",
    number="9230",
    month="July",
    year="1992"
  }

• Dexter Kozen. The Design and Analysis of Algorithms. Springer-Verlag, New York, 1991.
  [table of contents (.pdf)] [abstract] [bibtex] []

  @book{K91a,
    title="The Design and Analysis of Algorithms",
    author="Dexter Kozen",
    publisher="Springer-Verlag",
    address="New York",
    year="1991",
    isbn="0-387-97687-6",
    isbn="3-540-97687-6"
  }

  A graduate-level textbook on algorithms.

• Michael Ben-Or, Ephraim Feig, Dexter Kozen, and Prasoon Tiwari. Fast parallel algorithms for finding the roots of a polynomial with all real roots. In Proc. 18th Symp. Theory of Computing (STOC'86), pages 340-349. ACM, May 1986. (Subsumed by Michael Ben-Or, Ephraim Feig, Dexter Kozen, and Prasoon Tiwari. Fast parallel algorithms for finding the roots of a polynomial with all real roots. SIAM J. Comput., 17(6):1081-1092, 1988. doi:10.1137/0217069.)
  [bibtex] []

  @inproceedings{BFKT86a,
    author="Michael Ben-Or and Ephraim Feig and Dexter Kozen and Prasoon Tiwari",
    title="Fast parallel algorithms for finding the roots of a polynomial with all real roots",
    booktitle="Proc. 18th Symp. Theory of Computing (STOC'86)",
    organization="ACM",
    pages="340--349",
    month="May",
    year="1986"
  }

• Dexter Kozen. Fast parallel orthogonalization. SIGACT News, 18(2):47, Fall 1986.
  [full text (.pdf)] [bibtex] []

  @article{K86a,
    author="Dexter Kozen",
    title="Fast parallel orthogonalization",
    journal="SIGACT News",
    volume="18",
    number="2",
    pages="47",
    month="Fall",
    year="1986"
  }

• Dexter Kozen, Umesh Vazirani, and Vijay Vazirani. NC algorithms for comparability graphs, interval graphs, and unique perfect matching. In Maheshwari, editor, Proc. 5th Conf. Found. Software Technology and Theor. Comput. Sci., volume 206 of Lecture Notes in Computer Science, pages 496-503, New Delhi, December 1985. Springer-Verlag.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{KVV85a,
    author="Dexter Kozen and Umesh Vazirani and Vijay Vazirani",
    title="{{\em NC}} algorithms for comparability graphs, interval graphs, and unique perfect matching",
    booktitle="Proc. 5th Conf. Found. Software Technology and Theor. Comput. Sci.",
    editor="Maheshwari",
    publisher="Springer-Verlag",
    series="Lecture Notes in Computer Science",
    volume="206",
    address="New Delhi",
    pages="496--503",
    month="December",
    year="1985"
  }

  Laszlo Lovasz recently posed the following problem: ``Is there an NC algorithm for testing if a given graph has a unique perfect matching?'' We present such an algorithm for bipartite graphs. We also give NC algorithms for obtaining a transitive orientation of a comparability graph, and an interval representation of an interval graph. These enable us to obtain an NC algorithm for finding a maximum matching in an incomparability graph.

• Michael Ben-Or, Dexter Kozen, and John Reif. The complexity of elementary algebra and geometry. J. Comput. Syst. Sci., 32(2):251-264, 1986.
  [bibtex] []

  @article{BKR86,
    author="Michael Ben-Or and Dexter Kozen and John Reif",
    title="The complexity of elementary algebra and geometry",
    journal="J. Comput. Syst. Sci.",
    volume="32",
    number="2",
    pages="251--264",
    year="1986"
  }

• Dexter Kozen and Chee K. Yap. Algebraic cell decomposition in NC. In Proc. 26th Symp. Foundations of Computer Science (FOCS'85), pages 515-521. IEEE, October 1985.
  [full text (.pdf)] [bibtex] []

  @inproceedings{KY85,
    author="Dexter Kozen and Chee K. Yap",
    title="Algebraic cell decomposition in {{\em NC}}",
    booktitle="Proc. 26th Symp. Foundations of Computer Science (FOCS'85)",
    organization="IEEE",
    pages="515--521",
    month="October",
    year="1985"
  }

• Dexter Kozen. Pebblings, edgings, and equational logic. In Proc. 16th Symp. Theory of Computing (STOC'84), pages 428-435. ACM, May 1984.
  [bibtex] []

  @inproceedings{K84b,
    author="Dexter Kozen",
    title="Pebblings, edgings, and equational logic",
    booktitle="Proc. 16th Symp. Theory of Computing (STOC'84)",
    organization="ACM",
    pages="428--435",
    month="May",
    year="1984"
  }

• Michael Ben-Or, Dexter Kozen, and John Reif. The complexity of elementary algebra and geometry. In Proc. 16th Symp. Theory of Comput., pages 457-464. ACM, May 1984. (Subsumed by Michael Ben-Or, Dexter Kozen, and John Reif. The complexity of elementary algebra and geometry. J. Comput. Syst. Sci., 32(2):251-264, 1986.)
  [bibtex] []

  @inproceedings{BKR84a,
    author="Michael Ben-Or and Dexter Kozen and John Reif",
    title="The complexity of elementary algebra and geometry",
    booktitle="Proc. 16th Symp. Theory of Comput.",
    organization="ACM",
    pages="457--464",
    month="May",
    year="1984"
  }

• Ashok Chandra, Dexter Kozen, and Larry Stockmeyer. Alternation. J. Assoc. Comput. Mach., 28(1):114-133, 1981. doi:10.1145/322234.322243. (Subsumes Dexter Kozen. On parallelism in Turing machines. In Proc. 17th Symp. Found. Comput. Sci., pages 89-97. IEEE, October 1976.)
  [full text] [bibtex] []

  @article{CKS81a,
    author="Ashok Chandra and Dexter Kozen and Larry Stockmeyer",
    title="Alternation",
    journal="J. Assoc. Comput. Mach.",
    volume="28",
    number="1",
    pages="114--133",
    year="1981",
    doi="10.1145/322234.322243"
  }

• Dexter Kozen. Indexings of subrecursive classes. Theor. Comput. Sci., 11:277-301, 1980. (Subsumes Dexter Kozen. Indexings of subrecursive classes. In Proc. 10th Symp. Theory of Comput., pages 287-295. ACM, May 1978.)
  [bibtex] []

  @article{K80d,
    author="Dexter Kozen",
    title="Indexings of subrecursive classes",
    journal="Theor. Comput. Sci.",
    volume="11",
    pages="277--301",
    year="1980"
  }

• Dexter Kozen. Complexity of Boolean algebras. Theor. Comput. Sci., 10:221-247, 1980.
  [bibtex] []

  @article{K80c,
    author="Dexter Kozen",
    title="Complexity of {B}oolean algebras",
    journal="Theor. Comput. Sci.",
    volume="10",
    pages="221--247",
    year="1980"
  }

• Dexter Kozen and Michael Machtey. On relative diagonals. Technical Report RC8184, IBM Thomas J. Watson Research Center, April 1980.
  [bibtex] []

  @techreport{KM80a,
    author="Dexter Kozen and Michael Machtey",
    title="On relative diagonals",
    institution="IBM Thomas J. Watson Research Center",
    number="RC8184",
    month="April",
    year="1980"
  }

• Dexter Kozen. Automata and planar graphs. In Proc. 2nd Symp. Fund. Comput. Theory, pages 243-254, Berlin, September 1979.
  [bibtex] []

  @inproceedings{K79a,
    author="Dexter Kozen",
    title="Automata and Planar Graphs",
    booktitle="Proc. 2nd Symp. Fund. Comput. Theory",
    address="Berlin",
    pages="243--254",
    month="September",
    year="1979"
  }

• Dexter Kozen. Indexings of subrecursive classes. In Proc. 10th Symp. Theory of Comput., pages 287-295. ACM, May 1978. (Subsumed by Dexter Kozen. Indexings of subrecursive classes. Theor. Comput. Sci., 11:277-301, 1980.)
  [bibtex] []

  @inproceedings{K78b,
    author="Dexter Kozen",
    title="Indexings of subrecursive classes",
    booktitle="Proc. 10th Symp. Theory of Comput.",
    organization="ACM",
    pages="287--295",
    month="May",
    year="1978"
  }

• Manuel Blum and Dexter Kozen. On the power of the compass. In Proc. 19th Symp. Found. Comput. Sci., pages 132-142. IEEE, October 1978.
  [bibtex] []

  @inproceedings{BK78a,
    author="Manuel Blum and Dexter Kozen",
    title="On the power of the compass",
    booktitle="Proc. 19th Symp. Found. Comput. Sci.",
    organization="IEEE",
    pages="132--142",
    month="October",
    year="1978"
  }

• Dexter Kozen. A clique problem equivalent to graph isomorphism. SIGACT News, 10(2):50-52, June 1978.
  [bibtex] []

  @article{K78a,
    author="Dexter Kozen",
    title="A clique problem equivalent to graph isomorphism",
    journal="SIGACT News",
    organization="ACM",
    volume="10",
    number="2",
    pages="50--52",
    month="June",
    year="1978"
  }

• Dexter Kozen. Complexity of finitely presented algebras. PhD thesis, Computer Science Department, Cornell University, May 1977.
  [bibtex] []

  @phdthesis{K77d,
    author="Dexter Kozen",
    title="Complexity of finitely presented algebras",
    school="Computer Science Department, Cornell University",
    month="May",
    year="1977"
  }

• Dexter Kozen. Lower bounds for natural proof systems. In Proc. 18th Symp. Found. Comput. Sci., pages 254-266. IEEE, October 1977.
  [full text (.pdf)] [bibtex] []

  @inproceedings{K77c,
    author="Dexter Kozen",
    title="Lower bounds for natural proof systems",
    booktitle="Proc. 18th Symp. Found. Comput. Sci.",
    organization="IEEE",
    pages="254--266",
    month="October",
    year="1977"
  }

• Dexter Kozen. Complexity of finitely presented algebras. In Proc. 9th Symp. Theory of Comput., pages 164-177. ACM, May 1977.
  [full text (.pdf)] [bibtex] []

  @inproceedings{K77b,
    author="Dexter Kozen",
    title="Complexity of finitely presented algebras",
    booktitle="Proc. 9th Symp. Theory of Comput.",
    organization="ACM",
    pages="164--177",
    month="May",
    year="1977"
  }

• Dexter Kozen. Finitely presented algebras and the polynomial time hierarchy. Technical Report TR77-303, Computer Science Department, Cornell University, April 1977.
  [bibtex] []

  @techreport{K77a,
    author="Dexter Kozen",
    title="Finitely presented algebras and the polynomial time hierarchy",
    institution="Computer Science Department, Cornell University",
    number="TR77-303",
    month="April",
    year="1977"
  }

• Dexter Kozen. On parallelism in Turing machines. In Proc. 17th Symp. Found. Comput. Sci., pages 89-97. IEEE, October 1976. (Subsumed by Ashok Chandra, Dexter Kozen, and Larry Stockmeyer. Alternation. J. Assoc. Comput. Mach., 28(1):114-133, 1981. doi:10.1145/322234.322243.)
  [full text (.pdf)] [bibtex] []

  @inproceedings{K76a,
    author="Dexter Kozen",
    title="On parallelism in {T}uring machines",
    booktitle="Proc. 17th Symp. Found. Comput. Sci.",
    organization="IEEE",
    pages="89--97",
    month="October",
    year="1976"
  }

---

Coding Theory

• Keri D'Angelo and Dexter Kozen. Abstract Huffman coding and PIFO tree embeddings. In Data Compression Conference (DCC '23), March 2023.
  [full text] [abstract] [bibtex] []

  @inproceedings{DK23a,
    author="Keri D'Angelo and Dexter Kozen",
    title="Abstract {H}uffman Coding and {PIFO} Tree Embeddings",
    booktitle="Data Compression Conference (DCC '23)",
    month="March",
    year="2023"
  }

  Algorithms for deriving Huffman codes and the recently developed algorithm for compiling PIFO trees to trees of fixed shape (Mohan et al. 2022) are similar, but work with different underlying algebraic operations. In this paper, we exploit the monadic structure of prefix codes to create a generalized Huffman algorithm that has these two applications as special cases.

• Kenneth Andrews, Chris Heegard, and Dexter Kozen. Interleaver design methods for turbo codes. In Proc. International Symposium on Information Theory (ISIT'98), page 420. IEEE, August 1998.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{AHK98,
    title="Interleaver Design Methods for Turbo Codes",
    author="Kenneth Andrews and Chris Heegard and Dexter Kozen",
    booktitle="Proc. International Symposium on Information Theory (ISIT'98)",
    organization="IEEE",
    city="Cambridge, MA",
    month="August",
    year="1998",
    pages="420"
  }

  It is generally assumed that when a turbo decoder is operating at low bit error rates, error sequences have small Hamming weights. From this, and properties of turbo encoders, a mathematical structure is developed for interleaver design, permitting the identification of quantitatively optimal interleavers. Simulations show the math captures some but not all the essential characteristics of a successful interleaver. Modifying a random interleaver according to the mathematical ideas gives excellent simulation results.

• Kenneth Andrews, Chris Heegard, and Dexter Kozen. A theory of interleavers. Technical Report TR97-1634, Computer Science Department, Cornell University, June 1997.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{AHK97a,
    author="Kenneth Andrews and Chris Heegard and Dexter Kozen",
    title="A theory of interleavers",
    institution="Computer Science Department, Cornell University",
    number="TR97-1634",
    month="June",
    year="1997"
  }

  An interleaver is a hardware device commonly used in conjunction with error correcting codes to counteract the effect of burst errors. Interleavers are in widespread use and much is known about them from an engineering standpoint. In this paper we propose a mathematical model that provides a rigorous foundation for the theoretical study of interleavers. The model captures precisely such notions as block and convolutional interleavers, spread, periodicity, causality, latency, and memory usage. Using this model, we derive several optimality results on the latency and memory usage of interleavers. We describe a family of block interleavers and show that they are optimal with respect to latency among all block interleavers with a given spread. We also give tight upper and lower bounds on the memory requirements of interleavers.

---

Security

• Fred B. Schneider, Dexter Kozen, Greg Morrisett, and Andrew C. Myers. Language-based security for malicious mobile code. In Department of Defense Sponsored Information Security Research: New Methods for Protecting Against Cyber Threats, pages 477-494. Wiley, 2007.
  [full text (.pdf)] [abstract] [bibtex] []

  @incollection{SKMM07,
    author="Fred B. Schneider and Dexter Kozen and Greg Morrisett and Andrew C. Myers",
    title="Language-Based Security for Malicious Mobile Code",
    booktitle="Department of Defense Sponsored Information Security Research: New Methods for Protecting Against Cyber Threats",
    publisher="Wiley",
    city="Indianapolis",
    year="2007",
    pages="477--494"
  }

  A survey of language-based techniques for secure mobile processes.

• Matt Stillerman and Dexter Kozen. Demonstration: Efficient code certification for open firmware. In Proc. 3rd DARPA Information Survivability Conference and Exposition (DISCEX III), volume 2, pages 147-148. IEEE, IEEE Computer Society, Los Alamitos, CA, April 2003.
  [bibtex] []

  @inproceedings{SK03a,
    author="Matt Stillerman and Dexter Kozen",
    title="Demonstration: Efficient Code Certification for Open Firmware",
    booktitle="Proc. 3rd DARPA Information Survivability Conference and Exposition (DISCEX III)",
    volume="2",
    city="Washington, DC",
    month="April",
    year="2003",
    pages="147--148",
    organization="IEEE",
    publisher="IEEE Computer Society, Los Alamitos, CA"
  }

• Frank Adelstein, Dexter Kozen, and Matt Stillerman. Malicious code detection for open firmware. In Proc. 18th Computer Security Applications Conf. (ACSAC'02), pages 403-412, December 2002.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{AKS02,
    author="Frank Adelstein and Dexter Kozen and Matt Stillerman",
    title="Malicious Code Detection for Open Firmware",
    booktitle="Proc. 18th Computer Security Applications Conf. (ACSAC'02)",
    city="Las Vegas",
    month="December",
    year="2002",
    pages="403--412"
  }

  Malicious boot firmware is a largely unrecognized but significant security risk to our global information infrastructure. Since boot firmware executes before the operating system is loaded, it can easily circumvent any operating system-based security mechanism. Boot firmware programs are typically written by third-party device manufacturers and may come from various suppliers of unknown origin. In this paper we describe an approach to this problem based on load-time verification of onboard device drivers against a standard security policy designed to limit access to system resources. We also describe our ongoing effort to construct a prototype of this technique for Open Firmware boot platforms.

• Dexter Kozen. Language-based security. In M. Kutyowski, L. Pacholski, and T. Wierzbicki, editors, Proc. Conf. Mathematical Foundations of Computer Science (MFCS'99), volume 1672 of Lecture Notes in Computer Science, pages 284-298. Springer-Verlag, September 1999.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{K99b,
    author="Dexter Kozen",
    title="Language-based security",
    booktitle="Proc. Conf. Mathematical Foundations of Computer Science (MFCS'99)",
    city="Szklarska Por{\c{e}}ba, Poland",
    publisher="Springer-Verlag",
    series="Lecture Notes in Computer Science",
    volume="1672",
    editor="M. Kuty{\l}owski and L. Pacholski and T. Wierzbicki",
    pages="284--298",
    month="September",
    year="1999"
  }

  Security of mobile code is a major issue in today's global computing environment. When you download a program from an untrusted source, how can you be sure it will not do something undesirable? In this paper I will discuss a particular approach to this problem called language-based security. In this approach, security information is derived from a program written in a high-level language during the compilation process and is included in the compiled object. This extra security information can take the form of a formal proof, a type annotation, or some other form of certificate or annotation. It can be downloaded along with the object code and automatically verified before running the code locally, giving some assurance against certain types of failure or unauthorized activity. The verifier must be trusted, but the compiler, code, and certificate need not be. Java bytecode verification is an example of this approach. I will give an overview of some recent work in this area, including a particular effort in which we are trying to make the production of certificates and the verification as efficient and invisible as possible.

• Dexter Kozen. Efficient code certification. Technical Report TR98-1661, Computer Science Department, Cornell University, January 1998.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{K98a,
    author="Dexter Kozen",
    title="Efficient code certification",
    institution="Computer Science Department, Cornell University",
    number="TR98-1661",
    month="January",
    year="1998"
  }

  We introduce a simple and efficient approach to the certification of compiled code. We ensure a basic but nontrivial level of code safety, including control flow safety, memory safety, and stack safety. The system is designed to be simple, efficient, and (most importantly) relatively painless to incorporate into existing compilers. Although less expressive than the proof carrying code of Necula and Lee or typed assembly language of Morrisett et al., our certificates are by comparison extremely compact and relatively easy to produce and to verify. Unlike JAVA byte code, our system operates at the level of native code; it is not interpreted and no further compilation is necessary.

---

Other

• Chavdar Botev, Hubert Chao, Theodore Chao, Yim Cheng, Raymond Doyle, Sergey Grankin, Jon Guarino, Saikat Guha, PeiChen Lee, Dan Perry, Christopher Re, Ilya Rifkin, Tingyan Yuan, Dora Abdullah, Kathy Carpenter, David Gries, Dexter Kozen, Andrew Myers, David Schwartz, and Jayavel Shanmugasundaram. Supporting workflow in a course management system. In W. Dann et al., editor, Proc. 36th Technical Symposium on Computer Science Education (SIGCSE'05), pages 262-266. ACM SIGCSE, February 2005.
  [full text (.pdf)] [abstract] [bibtex] []

  @inproceedings{CMS05,
    author="Chavdar Botev and Hubert Chao and Theodore Chao and Yim Cheng and Raymond Doyle and Sergey Grankin and Jon Guarino and Saikat Guha and PeiChen Lee and Dan Perry and Christopher Re and Ilya Rifkin and Tingyan Yuan and Dora Abdullah and Kathy Carpenter and David Gries and Dexter Kozen and Andrew Myers and David Schwartz and Jayavel Shanmugasundaram",
    title="Supporting Workflow in a Course Management System",
    booktitle="Proc. 36th Technical Symposium on Computer Science Education (SIGCSE'05)",
    editor="W. Dann et al.",
    city="St. Louis",
    month="February",
    year="2005",
    publisher="ACM SIGCSE",
    pages="262--266"
  }

  CMS is a secure and scalable web-based course management system developed by the Cornell University Computer Science Department. The system was designed to simplify, streamline, and automate many aspects of the workflow associated with running a large course, such as course creation, importing students, management of student workgroups, online submission of assignments, assignment of graders, grading, handling regrade requests, and preparation of final grades. In contrast, other course management systems of which we are aware provide only specialized solutions for specific components, such as grading. CMS is increasingly widely used for course management at Cornell University. In this paper we articulate the principles we followed in designing the system and describe the features that users found most useful.

• Dexter Kozen. On teaching left-handed children to write. Technical Report TR87-844, Computer Science Department, Cornell University, June 1987.
  [full text (.pdf)] [abstract] [bibtex] []

  @techreport{K87a,
    author="Dexter Kozen",
    title="On teaching left-handed children to write",
    institution="Computer Science Department, Cornell University",
    number="TR87-844",
    month="June",
    year="1987"
  }

  A treatise on how to teach left-handed children to write comfortably and without smearing.

• Dexter Kozen. A Ramsey theorem with infinitely many colors. In Lenstra, Lenstra, and van Emde Boas, editors, Dopo Le Parole, pages 71-72. University of Amsterdam, Amsterdam, May 1984.
  [bibtex] []

  @incollection{K84a,
    author="Dexter Kozen",
    title="A {R}amsey theorem with infinitely many colors",
    booktitle="Dopo Le Parole",
    editor="Lenstra and Lenstra and van Emde Boas",
    publisher="University of Amsterdam",
    address="Amsterdam",
    pages="71--72",
    month="May",
    year="1984"
  }

©2021 Cornell University