Stephanie Weirich

Associate Professor of Computer and Information Science
School of Engineering and Applied Science
University of Pennsylvania

Ph.D. (2002) Computer Science
Cornell University

phone: 215.573.2821
fax: 215.898.0587
email: sweirich at cis.upenn.edu
office: 510 Levine Hall

I am spending the 2009-2010 academic year visiting the Cambridge Computer Laboratory and Microsoft Research Cambridge.

Quick Links

My publications (including drafts)
More information about my research (CV, talks, activities, etc.)
Penn's Programming Languages group
Submit papers to ICFP 2010
Submit papers to JAR special issue on the POPLmark Challenge
Tutorial on using Coq for PL Research from POPL 2008 and Oregon Summer School 2008
Help define the new Haskell standard: Haskell prime wiki

Current Research Projects

Dependently Typed Language: Programming in types. Next generation typed languages will allow programmers to explain to the type system why their code is correct. But we don't know what those languages will look like yet.

PIE: Notes on a prototype dependently-typed language
isEq: Dependent types and program equivalence
TRELLYS: Community-Based Design and Implementation of a Dependently Typed Programming Language

Type-directed programming: Programming with types. Defining functions via type information cuts down on boilerplate programming as many operations may be defined once, for all types of data. TDP is everywhere including:

in Agda: Arity-generic type-generic programming
in Haskell: RepLib: A library for derivable type classes and A Common Library for Generic Programming
in ML: AspectML and InforML
in Java: Type-Directed Java

Machine assistance for programming languages research: Designing and proving properties about programming languages is hard, but the proofs themselves are straightforward once you know how to set them up. At the same time, it is all too easy to miss the one little case that ruins the whole "proof". Modern proof assistants, such as Twelf, Coq, and Isabelle are good at expressing this sort of reasoning, but it is hard to know where to start. I've been working with the POPLmark team to issue challenge problems, organize a workshop, explore techniques for reasoning about binding, and develop educational materials about mechanizing programming language metatheory. Brian Aydemir maintains and develops a library for programming language metatheory (used in the Penn tutorials) and LNgen, a tool for automatically proving properties about binding.

Type inference for advanced type systems: Advanced type system features, such as first-class polymorphism, impredicative polymorphism and generalized algebraic datatypes, do not interact well with the standard algorithms for type inference in modern typed functional languages, such as ML and Haskell. Simon Peyton Jones, my students Dimitrios Vytiniotis, Geoffrey Washburn and I have been incorporating ideas from Local Type Inference to extend the Glasgow Haskell Compiler with support for these features.

Current Students

Graduated Students

Geoffrey Washburn (Dec. 2007, EPFL)
Dimitrios Vytiniotis (Aug. 2008, MSR Cambridge)

Recent Courses

Programming Languages and Techniques I (CSE/CIS 120)
    [Fall 08] [Spring 08] [Spring 07]
Advanced Topics in Programming Languages (CIS 670/CIS 700):
   [Spring 09] [Fall 06] [Spring 06] [Spring 05] [Fall 03] [Fall 02]
Software Foundations (CIS 500):
    [Fall 05] [Fall 04]
Principles of Programming Languages (CSE 340):
    [Spring 04] [Spring 03]

Other courses

Contact Information

office hours: By appointment

postal mail:
School of Engineering and Applied Science
Department of Computer and Information Science
Levine Hall
3330 Walnut Street
Philadelphia, PA 19104-6389

Advice for graduate students

Interested in Graduate Studies at Penn?

CISters

Advice for PhD students in CS
Academic job search advice and resources

Last Modified: Jul 1, 2008