kozen1997kleene:
  type: article
  title: Kleene Algebra with Tests
  author: Kozen, Dexter
  date: 1997-05
  page-range: 427-443
  url: https://dl.acm.org/doi/10.1145/256167.256195
  serial-number:
    doi: 10.1145/256167.256195
    issn: 0164-0925
  abstract: '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.'
  parent:
    type: periodical
    title: ACM Transactions on Programming Languages and Systems
    publisher: ACM
    issue: 3
    volume: 19