Now showing items 1-9 of 9

    • A Coalgebraic Decision Procedure for NetKAT 

      Foster, Nate; Kozen, Dexter; Milano, Matthew; Silva, Alexandra; Thompson, Laure (2014-03-26)
      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 ...
    • CoCaml: Programming with Coinductive Types 

      Jeannin, Jean-Baptiste; Kozen, Dexter; Silva, Alexandra (2012-12-31)
      We present CoCaml, a functional programming language extending OCaml, which allows us to define functions on coinductive datatypes parameterized by an equation solver. We provide numerous examples that attest to the ...
    • Completeness and Incompleteness in Nominal Kleene Algebra 

      Kozen, Dexter; Mamouras, Konstantinos; Silva, Alexandra (2014-11-14)
      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 ...
    • Left-Handed Completeness 

      Kozen, Dexter; Silva, Alexandra (2011-08-23)
      We give a new, significantly shorter proof of the completeness of the left-handed star rule of Kleene algebra. The proof reveals the rich interaction of algebra and coalgebra in the theory.
    • Nominal Kleene Coalgebra 

      Kozen, Dexter; Mamouras, Konstantinos; Petrisan, Daniela; Silva, Alexandra (2015-02-18)
      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 ...
    • On Moessner's Theorem 

      Kozen, Dexter; Silva, Alexandra (2011-06-12)
      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, ... Paasche's theorem is a generalization of Moessner's; by ...
    • Practical Coinduction 

      Kozen, Dexter; Silva, Alexandra (2012-11-11)
      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 ...
    • Probabilistic NetKAT 

      Foster, Nate; Kozen, Dexter; Mamouras, Konstantinos; Reitblatt, Mark; Silva, Alexandra (2015-07)
      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 ...
    • Well-Founded Coalgebras, Revisited 

      Jeannin, Jean-Baptiste; Kozen, Dexter; Silva, Alexandra (2013-05-24)
      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 ...