Stephanie Weirich's Publications

[1] Stephanie Weirich. Programming With Types. PhD thesis, Cornell University, 2002. Forthcoming.
[ bib ]
[2] Stephanie Weirich. Higher-order intensional type analysis. In Daniel Le Métayer, editor, 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, 2002. To appear.
[ bib | .ps | .pdf ]

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.

[3] Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type erasure semantics. In Journal of Functional Programming, 2002. To appear.
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.

[4] Stephanie Weirich. Encoding intensional type analysis. In D. Sands, editor, 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, volume 2028 of Lecture Notes in Computer Science, pages 92-106. Springer, 2001.
[ bib | http | .dvi | .ps | .pdf ]

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.

[5] Michael Hicks, Stephanie Weirich, and Karl Crary. Safe and flexible dynamic linking of native code. In R. Harper, editor, Types in Compilation: Third International Workshop, TIC 2000; Montreal, Canada, September 21, 2000; Revised Selected Papers, volume 2071 of Lecture Notes in Computer Science, pages 147-176. Springer, 2001.
[ bib | http | .ps.gz | .pdf ]

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.

[6] Stephanie Weirich. Type-safe cast: Functional pearl. In Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming, pages 58-67, Montreal, September 2000.
[ bib | .dvi | .ps | .pdf ]

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.

[7] Karl Crary and Stephanie Weirich. Resource bound certification. In Twenty-Seventh ACM Symposium on Principles of Programming Languages, pages 184-198, Boston, MA, January 2000.
[ bib | .dvi | .ps.gz | .pdf ]

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.

[8] Karl Crary and Stephanie Weirich. Flexible type analysis. In Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming, pages 233-248, Paris, September 1999.
[ bib | .dvi | .ps.gz | .pdf ]

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.

[9] Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In Second ACMSIGPLAN Workshop on Compiler Support for System Software, pages 25-35, Atlanta, GA, USA, May 1999. Published as INRIA research report number 0228, March 1999.
[ bib | .dvi | .ps.gz ]

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.

[10] Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type erasure semantics (extended version). Technical Report TR98-1721, Cornell University, November 1998. This paper is superceded by [3].
[ bib | .ps ]
[11] Karl Crary, Stephanie Weirich, and Greg Morrisett. Intensional polymorphism in type erasure semantics. In Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, volume 34 of ACM SIGPLAN Notices, pages 301-313, Baltimore, MD, September 1998. An extended and revised version of this paper is [3].
[ bib | .dvi | .ps ]
[12] Cormac Flanagan, Matthew Flatt, Shriram Krishnamurthi, Stephanie Weirich, and Matthias Felleisen. Catching bugs in the web of program invariants. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 23-32, 1996.
[ bib | http ]

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.


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