AUTHOR = {Stephanie Weirich},
  TITLE = {Programming With Types},
  SCHOOL = {Cornell University},
  NOTE = {Forthcoming},
  YEAR = 2002

  AUTHOR = {Stephanie Weirich},
  TITLE = {Higher-Order Intensional Type Analysis},
  BOOKTITLE = {Programming Languages and Systems: 11th
                 European Symposium on Programming, ESOP 2002 Held as
                 Part of the Joint European Conferences on Theory and
                 Practice of Software, ETAPS 2002 Grenoble, France, April
                 8-12, 2002},
  EDITOR = {Daniel Le M\'{e}tayer},
  NOTE = {To appear.},
  YEAR = 2002,
  PS = {http://www.cs.cornell.edu/sweirich/papers/hota/hota.ps},
  PDF = {http://www.cs.cornell.edu/sweirich/papers/hota/hota.pdf},
  ABSTRACT = {Intensional type analysis provides the ability to
     analyze abstracted types at run time. In this paper, we extend
     that ability to higher-order and kind-polymorphic type
     constructors. The resulting language is elegant and expressive:
     we show through examples how it extends the repertoire of
     polytypic functions that may be defined.}

  AUTHOR = {Karl Crary and Stephanie Weirich and Greg Morrisett},
  TITLE = {Intensional Polymorphism in Type Erasure Semantics},
  BOOKTITLE = {Journal of Functional Programming},
  YEAR = {2002},
  NOTE = {To appear.},
  ABSTRACT = {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, unboxed function
     arguments, polymorphic marshalling, and flattened data
     structures. To date, languages that support intensional
     polymorphism have required a type-passing (as opposed to
     type-erasure) interpretation where types are constructed and
     passed to polymorphic functions at run time. Unfortunately,
     type-passing suffers from a number of drawbacks; it requires
     duplication of constructs at the term and type levels, it
     prevents abstraction, and it severely complicates polymorphic
     closure conversion.  We present a type-theoretic framework that
     supports intensional polymorphism, but avoids many of the
     disadvantages of type passing. In our approach, run-time type
     information is represented by ordinary terms. This avoids the
     duplication problem, allows us to recover abstraction, and avoids
     complications with closure conversion. In addition, our type
     system provides another improvement in expressiveness; it allows
     unknown types to be refined in place thereby avoiding certain
     beta-expansions required by other frameworks.}

  AUTHOR = {Stephanie Weirich},
  TITLE = {Encoding Intensional Type Analysis},
  BOOKTITLE = {Programming Languages and Systems: 10th
                 European Symposium on Programming, ESOP 2001 Held as
                 Part of the Joint European Conferences on Theory and
                 Practice of Software, ETAPS 2001 Genova, Italy, April
                 2-6, 2001},
  YEAR = 2001,
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 2028,
  EDITOR = {D. Sands},
  PUBLISHER = {Springer},
  PAGES = {92--106},
  ANNOTE = {© 2001 Springer-Verlag. Minor corrections in local version.},
  URL = {http://link.springer.de/link/service/series/0558/tocs/t2028.htm},
  DVI = {http://www.cs.cornell.edu/sweirich/papers/depabs/depabs.dvi},
  PS = {http://www.cs.cornell.edu/sweirich/papers/depabs/depabs.ps},
  PDF = {http://www.cs.cornell.edu/sweirich/papers/depabs/depabs.pdf},
  ABSTRACT = {Languages for intensional type analysis permit ad-hoc
     polymorphism, or run-time analysis of types. However, such
     languages require complex, specialized constructs to support this
     operation, which hinder optimization and complicate the
     meta-theory of these languages. In this paper, we observe that
     such specialized operators need not be intrinsic to the language,
     and in fact, their operation may be simulated through standard
     encodings of iteration in the polymorphic lambda
     calculus. Therefore, we may more easily add intensional analysis
     operators to complicated languages via a translation semantics,
     instead of through language extension.}

  AUTHOR = {Stephanie Weirich},
  TITLE = {Type-Safe Cast: Functional Pearl},
  BOOKTITLE = {Proceedings of the Fifth {ACM SIGPLAN} International Conference on Functional Programming},
  YEAR = 2000,
  ADDRESS = {Montreal},
  PAGES = {58--67},
  ABSTRACT = {In a language with non-parametric or ad-hoc
    polymorphism, it is possible to determine the identity of a type
    variable at run time.  With this facility, we can write a function
    to convert a term from one abstract type to another, if the two
    hidden types are identical.  However, the naive implementation of
    this function requires that the term be destructed and rebuilt. In
    this paper, we show how to eliminate this overhead using
    higher-order type abstraction. We demonstrate this solution in two
    frameworks for ad-hoc polymorphism: intensional type analysis and
    type classes.},
  DVI = {http://www.cs.cornell.edu/sweirich/papers/cast/cast.dvi},
  PS = {http://www.cs.cornell.edu/sweirich/papers/cast/cast.ps},
  PDF = {http://www.cs.cornell.edu/sweirich/papers/cast/cast.pdf}

  AUTHOR = {Karl Crary and Stephanie Weirich},
  TITLE = {Resource Bound Certification},
  BOOKTITLE = {Twenty-Seventh  {ACM} Symposium on Principles of Programming Languages},
  PAGES = {184--198},
  YEAR = 2000,
  ADDRESS = {Boston, MA},
  DVI = {http://www.cs.cornell.edu/sweirich/papers/res/res.dvi},
  PDF = {http://www.cs.cornell.edu/sweirich/papers/res/res.pdf},
  PS = {http://www.cs.cornell.edu/sweirich/papers/res/res.ps.gz},
  ABSTRACT = {Various code certification systems allow the
    certification and static verification of a variety of important
    safety properties such as memory safety and control-flow
    safety. These systems provide valuable tools for verifying that
    untrusted and potentially malicious code is safe before execution.
    However, one important safety property that is not usually
    included is that programs adhere to specific bounds on resource
    consumption, such as running time.

    We present a decidable type system capable of specifying and
    certifying bounds on resource consumption. Our system makes two
    advances over previous resource bound certification systems, both
    of which are necessary for a practical system: we allow the
    execution time of programs and their subroutines to vary,
    depending on their arguments, and we provide a fully automatic
    compiler generating certified executables from source-level
    programs. The principal device in our approach is a strategy for
    simulating dependent types using sum and inductive kinds. }

  AUTHOR = {Greg Morrisett and Karl Crary and Neal Glew and Dan
                  Grossman and Richard Samuels and Frederick Smith and
                  David Walker and Stephanie Weirich and Steve
  TITLE = {{TALx86}: A Realistic Typed Assembly Language},
  BOOKTITLE = {Second  {ACM}{SIGPLAN} Workshop on Compiler Support for System Software},
  YEAR = 1999,
  PAGES = {25--35},
  NOTE = {Published as {INRIA} research report number 0228, March 1999.},
  ADDRESS = {Atlanta, GA, USA},
  DVI = {http://www.cs.cornell.edu/talc/papers/talx86-wcsss.dvi},
  PS = {http://www.cs.cornell.edu/talc/papers/talx86-wcsss.ps.gz},
  ABSTRACT = {The goal of typed assembly language (TAL) is to provide
     a low-level, statically typed target language that is better
     suited than Java bytecodes for supporting a wide variety of
     source languages and a number of important optimizations. In
     previous work, we formalized idealized versions of TAL and proved
     important safety properties about them. In this paper, we present
     our progress in defining and implementing a realistic typed
     assembly language called TALx86. The TALx86 instructions comprise
     a relatively complete fragment of the Intel IA32 (32-bit 80x86
     flat model) assembly language and are thus executable on
     processors such as the Intel Pentium. The type system for the
     language incorporates a number of advanced features necessary for
     safely compiling large programs to good code.

     To motivate the design of the type system, we demonstrate how
     various high-level language features are compiled to TALx86. For
     this purpose, we present a type-safe C-like language called

  AUTHOR = {Karl Crary and Stephanie Weirich},
  TITLE = {Flexible Type Analysis},
  BOOKTITLE = {Proceedings of the Fourth {ACM SIGPLAN} International Conference on Functional Programming},
  YEAR = 1999,
  ADDRESS = {Paris},
  PAGES = {233--248},
  ABSTRACT = {Run-time type dispatch enables a variety of advanced
     optimization techniques for polymorphic languages, including
     tag-free garbage collection, unboxed function arguments, and
     flattened data structures.  However, modern type-preserving
     compilers transform types between stages of compilation, making
     type dispatch prohibitively complex at low levels of typed
     compilation. It is crucial therefore for type analysis at these
     low levels to refer to the types of previous
     stages. Unfortunately, no current intermediate language supports
     this facility.

     To fill this gap, we present the language LX, which provides a
     rich language of type constructors supporting type analysis
     (possibly of previous-stage types) as a programming idiom. This
     language is quite flexible, supporting a variety of other
     applications such as analysis of quantified types, analysis with
     incomplete type information, and type classes. We also show that
     LX is compatible with a type-erasure semantics.},
  DVI = {http://www.cs.cornell.edu/sweirich/papers/lx/lxpaper.dvi},
  PS = {http://www.cs.cornell.edu/sweirich/papers/lx/lxpaper.ps.gz},
  PDF = {http://www.cs.cornell.edu/sweirich/papers/lx/lxpaper.pdf}

  AUTHOR = {Karl Crary and Stephanie Weirich and Greg Morrisett},
  TITLE = {Intensional Polymorphism in Type Erasure Semantics},
  BOOKTITLE = {Proceedings of the Third {ACM SIGPLAN} International Conference on Functional Programming},
  YEAR = 1998,
  VOLUME = 34,
  SERIES = {{ACM} {SIGPLAN} Notices},
  ADDRESS = {Baltimore, MD},
  PAGES = {301--313},
  NOTE = {An extended and revised version of this paper is \cite{crary+:intensional-journal}},
  DVI = {http://www.cs.cornell.edu/sweirich/papers/typepass/typepass.dvi},
  PS = {http://www.cs.cornell.edu/sweirich/papers/typepass/typepass.ps}

  AUTHOR = {Karl Crary and Stephanie Weirich and Greg Morrisett},
  TITLE = {Intensional Polymorphism in Type Erasure Semantics (Extended Version)},
  INSTITUTION = {Cornell University},
  YEAR = 1998,
  NUMBER = {TR98-1721},
  PS = {http://www.cs.cornell.edu/sweirich/papers/typepass/typepass-tr.ps},
  NOTE = {This paper is superceded by \cite{crary+:intensional-journal}.}

  AUTHOR = {Michael Hicks and Stephanie Weirich and Karl Crary},
  TITLE = {Safe and Flexible Dynamic Linking of Native Code},
  BOOKTITLE = {Types in Compilation: Third International Workshop, TIC 2000;
               Montreal, Canada, September 21, 2000; Revised Selected Papers},
  EDITOR = {R. Harper},
  PUBLISHER = {Springer},
  YEAR = 2001,
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 2071,
  PAGES = {147--176},
  ANNOTE = {Related technical report: Michael Hicks and Stephanie
     Weirich.  A calculus for dynamic loading. Technical Report
     MS-CIS-00-07, University of Pennsylvania, April 2000.},
  ABSTRACT = {We present the design and implementation of the first
     complete framework for flexible and safe dynamic linking of
     native code. Our approach extends Typed Assembly Language with a
     primitive for loading and typechecking code, which is flexible
     enough to support a variety of linking strategies, but simple
     enough that it does not significantly expand the trusted
     computing base. Using this primitive, along with the ability to
     compute with types, we show that we can program many existing
     dynamic linking approaches. As a concrete demonstration, we have
     used our framework to implement dynamic linking for a type-safe
     dialect of C, closely modeled after the standard linking facility
     for Unix C programs. Aside from the unavoidable cost of
     verification, our implementation performs comparably with the
     standard, untyped approach.},
  URL = {http://link.springer.de/link/service/series/0558/tocs/t2071.htm},
  PS = {http://www.cs.cornell.edu/sweirich/papers/dynlink/taldynlink.ps.gz},
  PDF = {http://www.cs.cornell.edu/sweirich/papers/dynlink/taldynlink.pdf}

  AUTHOR = {Cormac Flanagan and Matthew Flatt and Shriram
             Krishnamurthi and Stephanie Weirich and Matthias
  TITLE = {Catching Bugs in the Web of Program Invariants},
  BOOKTITLE = {Proceedings of the {ACM SIGPLAN} Conference on Programming Language Design and Implementation},
  YEAR = 1996,
  PAGES = {23--32},
  ABSTRACT = {MrSpidey is a user-friendly, interactive static
     debugger for Scheme. A static debugger supplements the standard
     debugger by analyzing the program and pinpointing those program
     operations tha may cause run-time errors suce as dereferencing
     the null pointer or applying non-functions. The program analysis
     of MrSpidey computes value set descriptions for each term in the
     program and constructs a value flow graph connecting the set
     descriptions. Using the set descriptions, MrSpidey can identify
     and highlight potentially erroneous program operations, whose
     cause the programmer can the explore by selectively exposing
     portions of the value flow graph.},
  PS = {http://www.cs.cornell.edu/sweirich/papers/pldi96-ffkwf_ps.gz}

This file has been generated by bibtex2html 1.51

This page is intended for the timely dissemination of scholarly works. These papers may not be reposted without the explicit written permission of the copyright holder. Many papers in this page appear ©Copyright 199x by ACM, Inc