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

Spring 2011 office hours: Wednesdays, 1:30-3PM

Quick Links

• My publications (including drafts)
• More information about my research (CV, talks, activities, etc.)
• Penn's Programming Languages group
  

• Fall 2011 - CIS 552
  
  
• Spring 2011 - CIS 120
  
  
• Attend PLDI 2011
  
• Submit papers to CPP 2011
• Submit papers to POPL 2012
  
• Nominate papers for SIGPLAN CACM Research Highlights
  

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 (Slides from PLPV 2010)
  
  

• 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:
• Spring School on Generic and Indexed Programming (my lecture notes)
• 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

• Chris Casinghino
• Vilhelm Sjöberg
• Brent Yorgey

Graduated Students

• Geoffrey Washburn (Dec. 2007, LogicBlox)
• 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):
   [Fall 2010] [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

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