NA01376_.WMF (8642 bytes)  Research

My main research interest is the study of Programming Languages.  My advisor is Greg Morrisett. I usually attend Cornell's PLDG.

Recent Publications (Complete list)

  • Stephanie Weirich. Higher-order intensional type analysis. To appear in European Symposium on Programming (ESOP02), Grenoble, France, April 2002.
    PS, PDF
  • Stephanie Weirich. Encoding intensional type analysis. In European Symposium on Programming (ESOP01), Genova, Italy, April 2001. Appears in LNCS 2028, © Springer-Verlag. Minor corrections in local version.
    BibTeX entry, Available here, DVI, PS
  • 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.
    BibTeX entry, DVI, PS

Service Activities

  • I have been on the program committee for the following conferences. 
  • I have reviewed papers for the following venues. I would be delighted to do more. 
    • Journals :  JFP, HOSC, Acta Informatica, TOPLAS
    • Conferences : ICFP, POPL, PLDI
    • Workshops : FOOL, ML Workshop, Haskell Workshop, PEPM

Invited Talks

  • Programming with Types 
    • OHSU/Oregon Graduate Institute, February 11, 2002.
    • University of Oregon, February 15, 2002.
    • University of Pennsylvania, February 19, 2002.
    • University of Virginia, February 28, 2002.
    • University of Maryland, March 4, 2002.
    • Northeastern University, March 13, 2002.
    • University of California, San Diego, March 15, 2002.
    • Purdue University, March 25, 2002.
    • University of Michigan, March 27, 2002.
    • University of Texas, April 2, 2002.
    • University of Colorado at Boulder, April 16, 2002.
    • Pennsylvania State University, April 19, 2002.
    • Massachusetts Institute of Technology, April 25, 2002.
    • Rice University, April 29, 2002.

Abstract:
Run-time type analysis is an increasingly important linguistic mechanism in modern programming languages. in language runtime systems, it is used to implement services such as accurate garbage collection, serialization, cloning and structural equality. Component frameworks rely on it to provide reflection mechanisms in order to discover and interact with program interfaces at run-time. This ability is also crucial in the design of large, distributed systems that must be flexible and robust enough to support frequent updates of new code and of new forms of data.

However, existing language support for run-time type analysis was designed for simple type systems and does not scale well to the sophisticvated type systems of modern and next-generation programming languages. These languages include complex type constructs such as first-class abstract types, recursive types, and objects, as well as a compile-time language to describe type parameterization. in this talk, I will show how the idea of interpreting that compile-time language at run time yields an expressive and elegant mechanism for describing type-directed operations.

  • "Research, Careers, and Computer Science: A Maryland Symposium." Maryland, November 16-17, 2001. Run-time type analysis for program verification.

    Abstract:
    Modern typed programming languages support type polymorphism: A function may be called without knowing the exact type of the argument. For example, in Java, the actual class of a method argument may be a subclass of the expected argument. In ML or Haskell, functions may be defined to operate over arguments of any type. Furthermore, many of these languages support the ability to determine the actual type of a value during the execution, if that type has been hidden. For example, in Java, the keyword "instanceof" determines if the actual class of an object is a subclass of the given type. 

    At the same time, advanced type systems allow the user to express and verify a large number of properties about her program. These properties might include checking that the code follows locking protocols, that the code uses a limited number of resources, that the code deallocates all of the memory that it allocates, or that all array accesses are within range. However, these properties are difficult to verify statically, and many programs may needlessly be rejected. In this talk, I will describe how technology for run-time type analysis can be used in a system for verifying program execution time.

  • IFIP WG 2.8, Åre, Sweden, April 2001. Polytypic Programming and Intensional Type (Constructor) Analysis.  This talk was a work-in-progress description of the paper, Higher-order intensional type analysis. 

Abstract:
Though useful for many applications such as marshaling, pickling, or garbage collection, intensional type analysis can't be used to represent standard polytypic functions like map. The problem is that these functions are defined on the structure of type constructors, not types. Recently, Hinze has shown how to systematically "lift" polytypic definitions over types to functions defined over type constructors. I will show how this idea plays out in the framework of intensional type analysis, allowing the run-time analysis of type constructors of any kind. The resulting system has several benefits: as well as permitting the definition of many new functions, the new rules are (in some sense) simpler, and they allow (via higher-order abstract syntax) the analysis of quantified types. However, this idea is not completely worked out: type-level type analysis does not interact well, and I can still think of one function that I can't write with this system.

Conference Presentations

Compiler Projects

 

 

 tal-logo.gif (5330 bytes)

[ HOME ]  research [ TEACHING ][COURSEWORK] [ PERSONAL]