Now showing items 11-20 of 307

    • Accepting Blame: Expressive Checked Exceptions 

      Zhang, Yizhou; Salvaneschi, Guido; Beightol, Quinn; Liskov, Barbara; Myers, Andrew C. (2016-04)
      Unhandled exceptions crash programs, so a compile-time check that exceptions are handled should in principle make software more reliable. But designers of some recent languages have argued that the benefits of statically ...
    • Genus: Making Generics Object-Oriented, Expressive, and Lightweight 

      Zhang, Yizhou; Loring, Matthew C.; Salvaneschi, Guido; Liskov, Barbara; Myers, Andrew C. (2015-06)
      The support for generic programming in modern object-oriented programming languages is awkward and lacks desirable expressive power. We introduce an expressive genericity mechanism that adds expressive power and strengthens ...
    • Kolmogorov Extension, Martingale Convergence, and Compositionality of Processes 

      Kozen, Dexter (2015-12-30)
      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 ...
    • Regular Expressions with Dynamic Name Binding 

      Kozen, Dexter; Milius, Stefan; Schröder, Lutz; Wißmann, Thorsten (2015-10-18)
      Nominal Kleene algebra (NKA) is a formalism to specify trace languages with name generation; it extends standard regular expressions with a name binding construct. NKA has been proved complete over a natural nominal language ...
    • 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 ...
    • Computational Election Verifiability: Definitions and an Analysis of Helios and JCJ 

      Smyth, Ben; Frink, Steven; Clarkson, Michael R. (2015-04-13)
      Definitions of election verifiability in the computational model of cryptography are proposed. The definitions formalize notions of voters verifying their own votes, auditors verifying the tally of votes, and auditors ...
    • Diagnosing Type Errors with Class 

      Zhang, Danfeng; Myers, Andrew C.; Vytiniotis, Dimitrios; Jones, Simon Peyton (2015-04-12)
      Type inference engines often give terrible error messages, and the more sophisticated the type system the worse the problem. We show that even with highly expressive type system implemented by the Glasgow Haskell Compiler ...
    • 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 ...
    • 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 ...
    • Merlin: A Language for Provisioning Network Resources 

      Soulé, Robert; Basu, Shrutarshi; Marandi, Parisa Jalili; Pedone, Fernando; Kleinberg, Robert; Sirer, Emin Gün; Foster, Nate (2014-06-25)
      This paper presents Merlin, a new framework for managing resources in software-defined networks. With Merlin, administrators express high-level policies using programs in a declarative language. The language includes logical ...