Now showing items 1-7 of 7

    • Alias Types 

      Smith, Frederick; Walker, David; Morrisett, Greg (Cornell University, 1999-10)
      Linear type systems allow destructive operations such as object deallocation and imperative updates of functional data structures. These operations and others, such as the ability to reuse memory at different types, are ...
    • Alias Types for Recursive Data Structures (Extended Version) 

      Walker, David; Morrisett, Greg (Cornell University, 2000-03-08)
      Linear type systems permit programmers to deallocate or explicitly recycle memory, but they are severly restricted by the fact that they admit no aliasing. This paper describes a pseudo-linear type system that allows a ...
    • Frenetic: A High-Level Language for OpenFlow Networks 

      Foster, Nate; Harrison, Rob; Freedman, Michael J.; Rexford, Jennifer; Walker, David (2010-12-02)
      Network administrators must configure network devices to simultaneously provide several interrelated services such as routing, load balancing, traffic monitoring, and access control. Unfortunately, most interfaces for ...
    • From System F to Typed Assembly Language (Extended Version) 

      Morrisett, Greg; Walker, David; Crary, Karl; Glew, Neal (Cornell University, 1997-11)
      We motivate the design of a statically typed assembly language (TAL) and present a type-preserving translation from System F to TAL. The TAL we present is based on a conventional RISC assembly language, but its static ...
    • NetKAT: Semantic Foundations for Networks 

      Anderson, Carolyn Jane; Foster, Nate; Guha, Arjun; Jeannin, Jean-Baptiste; Kozen, Dexter; Schlesinger, Cole; Walker, David (2013-10-11)
      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 ...
    • A Type System for Expressive Security Policies 

      Walker, David (Cornell University, 1999-04)
      {\em Certified code} is a general mechanism for enforcing security properties. In this paradigm, untrusted agent code carries annotations that allow a host to verify its trustworthiness. Before running the agent, the host ...
    • Typed Memory Management in a Calculus of Capabilities 

      Walker, David; Crary, Karl; Morrisett, Greg (Cornell University, 2000-02-02)
      Region-based memory management is an alternative to standard tracing garbage collection that makes potentially dangerous operations such as memory deallocation explicit but verifiably safe. In this article, we present a ...