Now showing items 1-5 of 5

    • 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 ...
    • 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 ...
    • The Complexity of Kleene Algebra with Tests 

      Cohen, Ernie; Kozen, Dexter; Smith, Frederick (Cornell University, 1996-07)
      Kleene algebras with tests provide a natural framework for equational specification and verification. Kleene algebras with tests and related systems have been used successfully in basic safety analysis, source-to-source ...
    • Kleene Algebra with Tests: Completeness and Decidability 

      Kozen, Dexter; Smith, Frederick (Cornell University, 1996-04)
      Kleene algebras with tests provide a rigorous framework for equational specification and verification. They have been used successfully in basic safety analysis, source-to-source program transformation, and concurrency ...
    • 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 ...