Now showing items 1-7 of 7

    • Admissibility of Fixpoint Induction over Partial Types 

      Crary, Karl (Cornell University, 1998-04)
      Partial types allow the reasoning about partial functions in type theory. The partial functions of main interest are recursively computed functions, which are commonly assigned types using fixpoint induction. However, ...
    • 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, ...
    • Programming Language Semantics in Foundational Type Theory 

      Crary, Karl (Cornell University, 1998-03)
      There are compelling benefits to using foundational type theory as a framework for programming language semantics. I give a semantics of an expressive programming calculus in the foundational type theory of Nuprl. Previous ...
    • Simple, Efficient Object Encoding using Intersection Types 

      Crary, Karl (Cornell University, 1998-04)
      I present a type-theoretic encoding of objects that interprets method dispatch by self-application (i.e., method functions are applied to the objects containing them) but still validates the expected subtyping relationships. ...
    • Type-Theoretic Methodology for Practical Programming Languages 

      Crary, Karl (Cornell University, 1998-08)
      The significance of type theory to the theory of programming languages has long been recognized. Advances in programming languages have often derived from understanding that stems from type theory. However, these ...
    • 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 ...