Now showing items 1-12 of 12

    • 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 ...
    • Certified In-lined Reference Monitoring on .Net 

      Hamlen, Kevin; Morrisett, Greg; Schneider, Fred (Cornell University, 2005-11-10)
      MOBILE is an extension of the .NET Common Intermediate Language that permits certified In-Lined Reference Monitoring on Microsoft .NET architectures. MOBILE programs have the useful property that if they are well-typed ...
    • Compiling for Runtime Code Generation (Extended Version) 

      Smith, Frederick; Grossman, Dan; Morrisett, Greg; Hornof, Luke; Jim, Trevor (Cornell University, 2000-10-27)
      Cyclone is a programming language that provides explicit support for dynamic specialization based on runtime code generation. To generate specialized code quickly, our Cyclone compiler uses a template based strategy ...
    • Computability Classes for Enforcement Mechanisms 

      Hamlen, Kevin W.; Morrisett, Greg; Schneider, Fred B. (Cornell University, 2003-08-26)
      A precise characterization of those security policies enforceable by program rewriting is given. This characterization exposes and rectifies problems in prior work on execution monitoring, yielding a more precise ...
    • 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 ...
    • Intensional Polymorphism in Type-Erasure Semantics 

      Crary, Karl; Weirich, Stephanie; Morrisett, Greg (Cornell University, 1998-11)
      Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, ...
    • A Language-Based Approach to Security 

      Schneider, Fred; Morrisett, Greg; Harper, Robert (Cornell University, 2000-11-20)
      Language-based security leverages program analysis and program rewriting to enforce security policies. The approach promises efficient enforcement of fine-grained access control policies and depends on a trusted computing ...
    • A Linearly Typed Assembly Language 

      Cheney, James; Morrisett, Greg (Cornell University, 2003-06-04)
      Today's type-safe low-level languages rely on garbage collection to recycle heap-allocated objects safely. We present LTAL, a safe, low-level, yet simple language that ``stands on its own'': it guarantees safe execution ...
    • Mostly-Copying Collection: A Viable Alternative to ConservativeMark-Sweep 

      Smith, Frederick; Morrisett, Greg (Cornell University, 1997-08)
      Many high-level language compilers generate C code and then invoke a C compiler to do code generation, register allocation, stack management, and low-level optimization. To date, most of these compilers link the resulting ...
    • Scalable Certification of Native Code: Experience from Compiling toTALx86 

      Grossman, Dan; Morrisett, Greg (Cornell University, 2000-02-02)
      Certifying compilation allows a compiler to produce annotations that prove that target code abides by a specified safety policy. An independent verifier can check the code without needing to trust the compiler. For such ...
    • 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 ...