My main research interest is the study of Programming Languages. My advisor is Greg Morrisett. I usually attend
- Stephanie Weirich. Higher-order intensional type analysis. To
appear in European Symposium on Programming (ESOP02), Grenoble,
France, April 2002.
Encoding intensional type analysis.
In European Symposium on Programming (ESOP01), Genova, Italy, April
Appears in LNCS 2028, © Springer-Verlag. Minor corrections in local
Type-safe cast : Functional pearl.
In Proceedings of the Fifth ACM SIGPLAN International
Conference on Functional Programming, pages 58-67, Montreal, September
- I have been on the program committee for the following conferences.
- International Conference on
Functional Programming (ICFP '02)
- Conference: October 3-5, 2002, Pittsburgh, PA, USA
- IFIP TC2
Working Conference on Generic Programming (WCGP '02)
- Conference: July 8 - July 13, 2002, Dagstuhl, Germany (with
- Conference: September 2, 2002, Firenze, Italy (part of PLI)
- I have reviewed papers for the following venues. I would be delighted to
- Journals : JFP, HOSC, Acta Informatica, TOPLAS
- Conferences : ICFP, POPL, PLDI
- Workshops : FOOL, ML Workshop, Haskell Workshop, PEPM
- 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.
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
- "Research, Careers, and Computer Science: A Maryland Symposium."
Maryland, November 16-17, 2001. Run-time type analysis for program
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.
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.