@PHDTHESIS{weirich:phd, AUTHOR = {Stephanie Weirich}, TITLE = {Programming With Types}, SCHOOL = {Cornell University}, NOTE = {Forthcoming}, YEAR = 2002 } @INPROCEEDINGS{weirich:hota, 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.} } @INPROCEEDINGS{crary+:intensional-journal, 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.} } @INPROCEEDINGS{weirich01, 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.} } @INPROCEEDINGS{weirich00, AUTHOR = {Stephanie Weirich}, TITLE = {Type-Safe Cast: Functional Pearl}, BOOKTITLE = {Proceedings of the Fifth {ACM SIGPLAN} International Conference on Functional Programming}, YEAR = 2000, MONTH = SEP, 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} } @INPROCEEDINGS{crary00, 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}, MONTH = JAN, 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. } } @INPROCEEDINGS{morrisett+:talx86, 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 Zdancewic}, TITLE = {{TALx86}: A Realistic Typed Assembly Language}, BOOKTITLE = {Second {ACM}{SIGPLAN} Workshop on Compiler Support for System Software}, YEAR = 1999, MONTH = MAY, 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 Popcorn.} } @INPROCEEDINGS{crary+:lx, AUTHOR = {Karl Crary and Stephanie Weirich}, TITLE = {Flexible Type Analysis}, BOOKTITLE = {Proceedings of the Fourth {ACM SIGPLAN} International Conference on Functional Programming}, YEAR = 1999, MONTH = SEP, 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} } @INPROCEEDINGS{crary+:intensional, 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}, MONTH = SEP, 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} } @TECHREPORT{crary98a, 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}, MONTH = NOV, PS = {http://www.cs.cornell.edu/sweirich/papers/typepass/typepass-tr.ps}, NOTE = {This paper is superceded by \cite{crary+:intensional-journal}.} } @INPROCEEDINGS{hicks00, 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} } @INPROCEEDINGS{flanagan96, AUTHOR = {Cormac Flanagan and Matthew Flatt and Shriram Krishnamurthi and Stephanie Weirich and Matthias Felleisen}, 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 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