Cornell's Faculty of Computing and Information Science (CIS) engages with every college at Cornell and shares the information revolution with every Cornell student to invent the fields of tomorrow.

Founded on the recognition that the ideas and technology of computing and information science are relevant to every academic discipline, CIS capitalizes on interdisciplinary collaboration to accelerate knowledge creation and discovery. At the center of Cornell's Information Campus, CIS bridges information and innovation.

For more information, go to Faculty of CIS Home Page.

Sub-communities within this community

Collections in this community

Recent Submissions

  • A Conversation with David Gries 

    Gries, David; Constable, Robert L. (Internet-First University Press, 2015-07-21)
  • Election Verifiability: Cryptographic Definitions and an Analysis of Helios and JCJ 

    Smyth, Ben; Frink, Steven; Clarkson, Michael R. (2015-08-06)
    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 ...
  • A Conversation with John E. Hopcroft 

    Hopcroft, John E.; Gries, David (Internet-First University Press, 2015-07-21)
    This ACM Turing Award recipient talks about research, textbooks, working with graduate students, his role as a senior statesman of his field and concludes with some words of wisdom.
  • A Conversation with Richard W. Conway 

    Conway, Richard W.; Gries, David (Internet-First University Press, 2015-07-21)
  • A Conversation with Robert L. Constable 

    Constable, Robert L.; Gries, David (Internet-First University Press, 2015-07-21)
  • A Conversation with Anil Nerode 

    Nerode, Anil; Gries, David (Internet-First University Press, 2014-10-16)
  • 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 ...
  • Genus: Making Generics Object-Oriented, Expressive, and Lightweight 

    Zhang, Yizhou; Loring, Matthew C.; Salvaneschi, Guido; Liskov, Barbara; Myers, Andrew C. (2015-04-15)
    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 ...
  • 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 ...
  • A Metrized Duality Theorem for Markov Processes 

    Kozen, Dexter; Mardare, Radu; Panangaden, Prakash (2014-05-21)
    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 ...
  • Fine-Grained User Privacy from Avenance Tags 

    Birrell, Eleanor; Schneider, Fred B. (2014-04-20)
    In the Internet, users interact with service providers; these interactions exchange information that might be considered private by the user. Existing schemes for expressing and enforcing user privacy on the Internet---notably ...
  • A Hardware Design Language for Efficient Control of Timing Channels 

    Zhang, Danfeng; Wang, Yao; Suh, G. Edward; Myers, Andrew C. (2014-04-10)
    Timing channels pose a real security risk, but methods are lacking for building systems without timing leaks. One reason is that low-level hardware features create timing channels; for example, caches enable probing attacks. ...
  • 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 ...
  • Kleene Algebra with Equations 

    Kozen, Dexter; Mamouras, Konstantinos (2014-02-27)
    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 ...
  • A Language for Securely Referencing Persistent Information in a Federated System 

    Liu, Jed; Myers, Andrew C. (2014-01-17)
    Referential integrity, which guarantees that named resources can be accessed when referenced, is an important property for reliability and security. In distributed systems, however, the attempt to provide referential ...
  • KAT + B! 

    Grathwohl, Niels Bjørn Bugge; Kozen, Dexter; Mamouras, Konstantinos (2014-01-08)
    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 ...

View more

Statistics

RSS Feeds